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