The cat chases the squirrel. The cat eats the mouse. The cow is green. The mouse is red. The squirrel chases the cow. The squirrel eats the mouse. The squirrel is round. If someone chases the squirrel and they chase the cow then they chase the cat. If someone is round and red then they chase the mouse. If someone eats the cow then the cow eats the cat. If someone chases the cow then they eat the mouse. If someone is round then they visit the cat. If someone is round then they chase the squirrel. If the cat is blue and the cat chases the squirrel then the squirrel chases the cow. If the squirrel chases the cat and the cat chases the squirrel then the cat chases the mouse.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cow is green.
("cow" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone chases the squirrel and they chase the cow then they chase the cat.
((("someone" "chases" "squirrel" "+") ("someone" "chases" "cow" "+")) -> ("someone" "chases" "cat" "+"))
If someone is round and red then they chase the mouse.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "chases" "mouse" "+"))
If someone eats the cow then the cow eats the cat.
((("someone" "eats" "cow" "+")) -> ("cow" "eats" "cat" "+"))
If someone chases the cow then they eat the mouse.
((("someone" "chases" "cow" "+")) -> ("someone" "eats" "mouse" "+"))
If someone is round then they visit the cat.
((("someone" "is" "round" "+")) -> ("someone" "visits" "cat" "+"))
If someone is round then they chase the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "chases" "squirrel" "+"))
If the cat is blue and the cat chases the squirrel then the squirrel chases the cow.
((("cat" "is" "blue" "+") ("cat" "chases" "squirrel" "+")) -> ("squirrel" "chases" "cow" "+"))
If the squirrel chases the cat and the cat chases the squirrel then the cat chases the mouse.
((("squirrel" "chases" "cat" "+") ("cat" "chases" "squirrel" "+")) -> ("cat" "chases" "mouse" "+"))
The squirrel eats the mouse.
True
1
proof
[(triple6 OR ((triple5) -> rule4))]
("squirrel" "eats" "mouse" "+")
triple6
((triple5) -> (rule4 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel does not eat the mouse.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule4))]
("squirrel" "eats" "mouse" "-")
triple6
((triple5) -> (rule4 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel chases the squirrel.
True
2
proof
[(((triple7) -> rule6))]
("squirrel" "chases" "squirrel" "+")
((triple7) -> (rule6 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel does not chase the squirrel.
False
2
inv-proof
[(((triple7) -> rule6))]
("squirrel" "chases" "squirrel" "-")
((triple7) -> (rule6 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel chases the cat.
True
4
proof
[(((((triple7) -> rule6) triple5) -> rule1))]
("squirrel" "chases" "cat" "+")
((((triple7) -> (rule6 % int2)) triple5) -> (rule1 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel does not chase the cat.
False
4
inv-proof
[(((((triple7) -> rule6) triple5) -> rule1))]
("squirrel" "chases" "cat" "-")
((((triple7) -> (rule6 % int2)) triple5) -> (rule1 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The cat chases the mouse.
True
6
proof
[(((((((triple7) -> rule6) triple5) -> rule1) triple1) -> rule8))]
("cat" "chases" "mouse" "+")
((((((triple7) -> (rule6 % int3)) triple5) -> (rule1 % int2)) triple1) -> (rule8 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The cat does not chase the mouse.
False
6
inv-proof
[(((((((triple7) -> rule6) triple5) -> rule1) triple1) -> rule8))]
("cat" "chases" "mouse" "-")
((((((triple7) -> (rule6 % int3)) triple5) -> (rule1 % int2)) triple1) -> (rule8 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The cow does not eat the mouse.
Unknown
inv-rconc
[@1: The cow eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "mouse" "-")
The cow eats the cat.
Unknown
rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "cat" "+")
The cow does not visit the cat.
Unknown
inv-rconc
[@1: The cow visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "visits" "cat" "-")
The mouse visits the cat.
Unknown
rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "cat" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The squirrel eats the cat.
Unknown
random
[@0: The squirrel eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "cat" "+")
The cow does not visit the squirrel.
Unknown
inv-random
[@0: The cow visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "squirrel" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The cat chases the squirrel.[(triple1)] The cat eats the mouse.[(triple2)] The cow is green.[(triple3)] The mouse is red.[(triple4)] The squirrel chases the cow.[(triple5)] The squirrel eats the mouse.[(triple6 OR ((triple5) -> rule4))] The squirrel is round.[(triple7)] @1: The squirrel chases the squirrel.[(((triple7) -> rule6))] The squirrel visits the cat.[(((triple7) -> rule5))] @2: The squirrel chases the cat.[(((((triple7) -> rule6) triple5) -> rule1))] @3: The cat chases the mouse.[(((((((triple7) -> rule6) triple5) -> rule1) triple1) -> rule8))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
triple4
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple5
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple6
((triple5) -> (rule4 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
triple7
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple7) -> (rule6 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple7) -> (rule5 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
((((triple7) -> (rule6 % int2)) triple5) -> (rule1 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((((((triple7) -> (rule6 % int3)) triple5) -> (rule1 % int2)) triple1) -> (rule8 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3