The cat chases the squirrel. The cat is not green. The cat needs the mouse. The mouse chases the cat. The mouse is nice. The mouse is rough. The mouse likes the cat. The mouse likes the squirrel. The squirrel is rough. The squirrel needs the cat. If something chases the squirrel then it chases the mouse. If something chases the mouse and the mouse is not rough then the mouse chases the squirrel. If the squirrel is green then the squirrel needs the cat. If something chases the mouse then it does not like the mouse. If something needs the mouse then it chases the cat. If the mouse likes the squirrel and the mouse is rough then the mouse needs the squirrel. If something likes the squirrel and it does not like the mouse then the mouse likes the squirrel. If something needs the squirrel then the squirrel needs the mouse.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat is not green.
("cat" "is" "green" "-")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If something chases the squirrel then it chases the mouse.
((("something" "chases" "squirrel" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the mouse and the mouse is not rough then the mouse chases the squirrel.
((("something" "chases" "mouse" "+") ("mouse" "is" "rough" "~")) -> ("mouse" "chases" "squirrel" "+"))
If the squirrel is green then the squirrel needs the cat.
((("squirrel" "is" "green" "+")) -> ("squirrel" "needs" "cat" "+"))
If something chases the mouse then it does not like the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "likes" "mouse" "-"))
If something needs the mouse then it chases the cat.
((("something" "needs" "mouse" "+")) -> ("something" "chases" "cat" "+"))
If the mouse likes the squirrel and the mouse is rough then the mouse needs the squirrel.
((("mouse" "likes" "squirrel" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "needs" "squirrel" "+"))
If something likes the squirrel and it does not like the mouse then the mouse likes the squirrel.
((("something" "likes" "squirrel" "+") ("something" "likes" "mouse" "~")) -> ("mouse" "likes" "squirrel" "+"))
If something needs the squirrel then the squirrel needs the mouse.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "+"))
The squirrel is rough.
True
1
proof
[(triple9)]
("squirrel" "is" "rough" "+")
triple9
The cat does not need the mouse.
False
1
inv-proof
[(triple3)]
("cat" "needs" "mouse" "-")
triple3
The cat chases the cat.
True
2
proof
[(((triple3) -> rule5))]
("cat" "chases" "cat" "+")
((triple3) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The mouse does not need the squirrel.
False
3
inv-proof
[(((triple8 triple6) -> rule6))]
("mouse" "needs" "squirrel" "-")
((triple8 triple6) -> (rule6 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel needs the mouse.
True
4
proof
[(((((triple8 triple6) -> rule6)) -> rule8))]
("squirrel" "needs" "mouse" "+")
((((triple8 triple6) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel does not need the mouse.
False
4
inv-proof
[(((((triple8 triple6) -> rule6)) -> rule8))]
("squirrel" "needs" "mouse" "-")
((((triple8 triple6) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel chases the cat.
True
5
proof
[(((((((triple8 triple6) -> rule6)) -> rule8)) -> rule5))]
("squirrel" "chases" "cat" "+")
((((((triple8 triple6) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel does not chase the cat.
False
5
inv-proof
[(((((((triple8 triple6) -> rule6)) -> rule8)) -> rule5))]
("squirrel" "chases" "cat" "-")
((((((triple8 triple6) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel does not chase the mouse.
Unknown
inv-rconc
[@1: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "mouse" "-")
The mouse chases the squirrel.
Unknown
rconc
[@1: The mouse chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "squirrel" "+")
The mouse does not chase the mouse.
Unknown
inv-rconc
[@2: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The squirrel likes the mouse.
Unknown
random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The cat chases the squirrel.[(triple1)] The cat is not green.[(triple2)] The cat needs the mouse.[(triple3)] The mouse chases the cat.[(triple4)] The mouse is nice.[(triple5)] The mouse is rough.[(triple6)] The mouse likes the cat.[(triple7)] The mouse likes the squirrel.[(triple8)] The squirrel is rough.[(triple9)] The squirrel needs the cat.[(triple10)] @1: The cat chases the cat.[(((triple3) -> rule5))] The cat chases the mouse.[(((triple1) -> rule1))] The mouse needs the squirrel.[(((triple8 triple6) -> rule6))] @2: The cat does not like the mouse.[(((((triple1) -> rule1)) -> rule4))] The squirrel needs the mouse.[(((((triple8 triple6) -> rule6)) -> rule8))] @3: The squirrel chases the cat.[(((((((triple8 triple6) -> rule6)) -> rule8)) -> rule5))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat is not green.
("cat" "is" "green" "-")
triple2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple4
The mouse is nice.
("mouse" "is" "nice" "+")
triple5
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple7
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple8
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple9
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple10
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple3) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple1) -> (rule1 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((triple8 triple6) -> (rule6 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The cat does not like the mouse.
("cat" "likes" "mouse" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat does not like the mouse.
("cat" "likes" "mouse" "-")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((((triple8 triple6) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
((((((triple8 triple6) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3