The cat chases the rabbit. The cat is green. The cat is rough. The cat needs the rabbit. The cat visits the rabbit. The rabbit chases the cat. The rabbit needs the cat. If something is rough then it needs the rabbit. If something chases the cat then it is rough. All green things are blue. If something visits the cat then the cat needs the rabbit. If something is rough then it visits the cat. If the rabbit needs the cat and the rabbit visits the cat then the rabbit chases the cat. If something needs the cat and it visits the cat then the cat visits the rabbit. If the rabbit needs the cat and the rabbit chases the cat then the cat is blue.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something is rough then it needs the rabbit.
((("something" "is" "rough" "+")) -> ("something" "needs" "rabbit" "+"))
If something chases the cat then it is rough.
((("something" "chases" "cat" "+")) -> ("something" "is" "rough" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something visits the cat then the cat needs the rabbit.
((("something" "visits" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
If something is rough then it visits the cat.
((("something" "is" "rough" "+")) -> ("something" "visits" "cat" "+"))
If the rabbit needs the cat and the rabbit visits the cat then the rabbit chases the cat.
((("rabbit" "needs" "cat" "+") ("rabbit" "visits" "cat" "+")) -> ("rabbit" "chases" "cat" "+"))
If something needs the cat and it visits the cat then the cat visits the rabbit.
((("something" "needs" "cat" "+") ("something" "visits" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If the rabbit needs the cat and the rabbit chases the cat then the cat is blue.
((("rabbit" "needs" "cat" "+") ("rabbit" "chases" "cat" "+")) -> ("cat" "is" "blue" "+"))
The cat is green.
True
1
proof
[(triple2)]
("cat" "is" "green" "+")
triple2
The rabbit does not chase the cat.
False
1
inv-proof
[(triple6)]
("rabbit" "chases" "cat" "-")
triple6
The rabbit is rough.
True
2
proof
[(((triple6) -> rule2))]
("rabbit" "is" "rough" "+")
((triple6) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cat is not blue.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple7 triple6) -> rule8))]
("cat" "is" "blue" "-")
((triple2) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple7 triple6) -> (rule8 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
@0: The cat chases the rabbit.[(triple1)] The cat is green.[(triple2)] The cat is rough.[(triple3)] The cat needs the rabbit.[(triple4 OR ((triple3) -> rule1) OR ((((triple3) -> rule5)) -> rule4) OR ((((((triple6) -> rule2)) -> rule5)) -> rule4))] The cat visits the rabbit.[(triple5 OR ((triple7 ((((triple6) -> rule2)) -> rule5)) -> rule7))] The rabbit chases the cat.[(triple6)] The rabbit needs the cat.[(triple7)] @1: The cat is blue.[(((triple2) -> rule3) OR ((triple7 triple6) -> rule8))] The cat visits the cat.[(((triple3) -> rule5))] The rabbit is rough.[(((triple6) -> rule2))] @2: The rabbit needs the rabbit.[(((((triple6) -> rule2)) -> rule1))] The rabbit visits the cat.[(((((triple6) -> rule2)) -> rule5))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple4
((triple3) -> (rule1 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple5
((triple7 ((((triple6) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple6
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple7
The cat is blue.
("cat" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple7 triple6) -> (rule8 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple3) -> (rule5 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple6) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2