The cat needs the cow. The cow likes the cat. The squirrel visits the cow. Young people are not nice. If the squirrel visits the cat then the squirrel likes the cat. If someone likes the cat then the cat is young. If someone is big and they like the squirrel then the squirrel likes the cow. If someone likes the cat and the cat is not nice then the cat likes the squirrel. If the squirrel likes the cow and the cow is not blue then the cow needs the cat.
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
Young people are not nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "-"))
If the squirrel visits the cat then the squirrel likes the cat.
((("squirrel" "visits" "cat" "+")) -> ("squirrel" "likes" "cat" "+"))
If someone likes the cat then the cat is young.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "young" "+"))
If someone is big and they like the squirrel then the squirrel likes the cow.
((("someone" "is" "big" "+") ("someone" "likes" "squirrel" "+")) -> ("squirrel" "likes" "cow" "+"))
If someone likes the cat and the cat is not nice then the cat likes the squirrel.
((("someone" "likes" "cat" "+") ("cat" "is" "nice" "~")) -> ("cat" "likes" "squirrel" "+"))
If the squirrel likes the cow and the cow is not blue then the cow needs the cat.
((("squirrel" "likes" "cow" "+") ("cow" "is" "blue" "~")) -> ("cow" "needs" "cat" "+"))
The cat needs the cow.
True
1
proof
[(triple1)]
("cat" "needs" "cow" "+")
triple1
The cat does not need the cow.
False
1
inv-proof
[(triple1)]
("cat" "needs" "cow" "-")
triple1
The cat is young.
True
2
proof
[(((triple2) -> rule3))]
("cat" "is" "young" "+")
((triple2) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is not young.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "is" "young" "-")
((triple2) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is not nice.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("cat" "is" "nice" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is nice.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("cat" "is" "nice" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat likes the squirrel.
True
5
proof
[(((triple2 ((((triple2) -> rule3)) -> rule1)) -> rule5))]
("cat" "likes" "squirrel" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat is not nice.
("cat" "is" "nice" "-")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cat does not like the squirrel.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule3)) -> rule1)) -> rule5))]
("cat" "likes" "squirrel" "-")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat is not nice.
("cat" "is" "nice" "-")
int2
The cat is young.
("cat" "is" "young" "+")
int3
The cow does not need the cat.
Unknown
inv-rconc
[@1: The cow needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "needs" "cat" "-")
The squirrel likes the cat.
Unknown
rconc
[@1: The squirrel likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "cat" "+")
The squirrel does not like the cow.
Unknown
inv-rconc
[@1: The squirrel likes the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "likes" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The cat does not need the squirrel.
Unknown
inv-random
[@0: The cat needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "squirrel" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The squirrel does not need the cat.
Unknown
inv-random
[@0: The squirrel needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cat" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cat needs the cow.[(triple1)] The cow likes the cat.[(triple2)] The squirrel visits the cow.[(triple3)] @1: The cat is young.[(((triple2) -> rule3))] @2: The cat is not nice.[(((((triple2) -> rule3)) -> rule1))] @3: The cat likes the squirrel.[(((triple2 ((((triple2) -> rule3)) -> rule1)) -> rule5))]
The cat needs the cow.
("cat" "needs" "cow" "+")
triple1
The cow likes the cat.
("cow" "likes" "cat" "+")
triple2
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
((triple2) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is not nice.
("cat" "is" "nice" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat is not nice.
("cat" "is" "nice" "-")
int2
The cat is young.
("cat" "is" "young" "+")
int3