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