The cat is cold. The cat is kind. The cat visits the rabbit. The cow eats the cat. The cow is round. The cow needs the rabbit. The rabbit eats the cow. The rabbit is rough. The rabbit is round. The rabbit needs the cat. If something is round then it needs the cat. If something needs the rabbit then it eats the cat. If something visits the rabbit and it is rough then the rabbit eats the cow. If something visits the cat and the cat visits the rabbit then it visits the cow. If the cat visits the rabbit then the rabbit eats the cat. If something needs the cat and the cat is cold then it eats the rabbit.
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something is round then it needs the cat.
((("something" "is" "round" "+")) -> ("something" "needs" "cat" "+"))
If something needs the rabbit then it eats the cat.
((("something" "needs" "rabbit" "+")) -> ("something" "eats" "cat" "+"))
If something visits the rabbit and it is rough then the rabbit eats the cow.
((("something" "visits" "rabbit" "+") ("something" "is" "rough" "+")) -> ("rabbit" "eats" "cow" "+"))
If something visits the cat and the cat visits the rabbit then it visits the cow.
((("something" "visits" "cat" "+") ("cat" "visits" "rabbit" "+")) -> ("something" "visits" "cow" "+"))
If the cat visits the rabbit then the rabbit eats the cat.
((("cat" "visits" "rabbit" "+")) -> ("rabbit" "eats" "cat" "+"))
If something needs the cat and the cat is cold then it eats the rabbit.
((("something" "needs" "cat" "+") ("cat" "is" "cold" "+")) -> ("something" "eats" "rabbit" "+"))
The cat is cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "+")
triple1
The cow does not eat the cat.
False
1
inv-proof
[(triple4 OR ((triple6) -> rule2))]
("cow" "eats" "cat" "-")
triple4
((triple6) -> (rule2 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The rabbit eats the cat.
True
2
proof
[(((triple3) -> rule5))]
("rabbit" "eats" "cat" "+")
((triple3) -> (rule5 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((triple10 triple1) -> rule6) OR ((((triple9) -> rule1) triple1) -> rule6))]
("rabbit" "eats" "rabbit" "-")
((triple10 triple1) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((((triple9) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The cow eats the rabbit.
True
4
proof
[(((((triple5) -> rule1) triple1) -> rule6))]
("cow" "eats" "rabbit" "+")
((((triple5) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
The cow does not eat the rabbit.
False
4
inv-proof
[(((((triple5) -> rule1) triple1) -> rule6))]
("cow" "eats" "rabbit" "-")
((((triple5) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
The cat does not visit the cow.
Unknown
inv-rconc
[@1: The cat visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "cow" "-")
The cat eats the rabbit.
Unknown
rconc
[@2: The cat eats the rabbit.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("cat" "eats" "rabbit" "+")
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "cat" "-")
The cat eats the cow.
Unknown
random
[@0: The cat eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cow" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The cat is cold.[(triple1)] The cat is kind.[(triple2)] The cat visits the rabbit.[(triple3)] The cow eats the cat.[(triple4 OR ((triple6) -> rule2))] The cow is round.[(triple5)] The cow needs the rabbit.[(triple6)] The rabbit eats the cow.[(triple7)] The rabbit is rough.[(triple8)] The rabbit is round.[(triple9)] The rabbit needs the cat.[(triple10 OR ((triple9) -> rule1))] @1: The cow needs the cat.[(((triple5) -> rule1))] The rabbit eats the cat.[(((triple3) -> rule5))] The rabbit eats the rabbit.[(((triple10 triple1) -> rule6) OR ((((triple9) -> rule1) triple1) -> rule6))] @2: The cow eats the rabbit.[(((((triple5) -> rule1) triple1) -> rule6))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple3
The cow eats the cat.
("cow" "eats" "cat" "+")
triple4
((triple6) -> (rule2 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow is round.
("cow" "is" "round" "+")
triple5
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple6
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple10
((triple9) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
((triple5) -> (rule1 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
((triple3) -> (rule5 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple10 triple1) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((((triple9) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((((triple5) -> (rule1 % int2)) triple1) -> (rule6 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2