The cat does not eat the squirrel. The cat is big. The cat is blue. The cat is rough. The cat is round. The cat is young. The cat needs the squirrel. The cat does not see the squirrel. The squirrel is blue. The squirrel is not rough. The squirrel is round. The squirrel does not see the cat. If someone is big then they are young. If someone eats the cat and they need the cat then the cat is blue. If someone is blue then they need the cat. If someone needs the cat then they are big. If the squirrel needs the cat and the cat sees the squirrel then the squirrel does not see the cat. If someone eats the cat and they eat the squirrel then the squirrel does not need the cat. If someone needs the cat and the cat is not young then they are round. If someone is round and not blue then they need the squirrel.
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is not rough.
("squirrel" "is" "rough" "-")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone eats the cat and they need the cat then the cat is blue.
((("someone" "eats" "cat" "+") ("someone" "needs" "cat" "+")) -> ("cat" "is" "blue" "+"))
If someone is blue then they need the cat.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "cat" "+"))
If someone needs the cat then they are big.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "big" "+"))
If the squirrel needs the cat and the cat sees the squirrel then the squirrel does not see the cat.
((("squirrel" "needs" "cat" "+") ("cat" "sees" "squirrel" "+")) -> ("squirrel" "sees" "cat" "-"))
If someone eats the cat and they eat the squirrel then the squirrel does not need the cat.
((("someone" "eats" "cat" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "needs" "cat" "-"))
If someone needs the cat and the cat is not young then they are round.
((("someone" "needs" "cat" "+") ("cat" "is" "young" "~")) -> ("someone" "is" "round" "+"))
If someone is round and not blue then they need the squirrel.
((("someone" "is" "round" "+") ("someone" "is" "blue" "~")) -> ("someone" "needs" "squirrel" "+"))
The cat is round.
True
1
proof
[(triple5)]
("cat" "is" "round" "+")
triple5
The cat is not rough.
False
1
inv-proof
[(triple4)]
("cat" "is" "rough" "-")
triple4
The squirrel needs the cat.
True
2
proof
[(((triple9) -> rule3))]
("squirrel" "needs" "cat" "+")
((triple9) -> (rule3 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The squirrel does not need the cat.
False
2
inv-proof
[(((triple9) -> rule3))]
("squirrel" "needs" "cat" "-")
((triple9) -> (rule3 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The squirrel is big.
True
3
proof
[(((((triple9) -> rule3)) -> rule4))]
("squirrel" "is" "big" "+")
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The squirrel is not big.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule4))]
("squirrel" "is" "big" "-")
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The squirrel is young.
True
4
proof
[(((((((triple9) -> rule3)) -> rule4)) -> rule1))]
("squirrel" "is" "young" "+")
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3
The squirrel is not young.
False
4
inv-proof
[(((((((triple9) -> rule3)) -> rule4)) -> rule1))]
("squirrel" "is" "young" "-")
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel eats the cat.
Unknown
random
[@0: The squirrel eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "cat" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat does not eat the squirrel.[(triple1)] The cat does not see the squirrel.[(triple8)] The cat is big.[(triple2 OR ((((triple3) -> rule3)) -> rule4))] The cat is blue.[(triple3)] The cat is rough.[(triple4)] The cat is round.[(triple5)] The cat is young.[(triple6 OR ((triple2) -> rule1) OR ((((((triple3) -> rule3)) -> rule4)) -> rule1))] The cat needs the squirrel.[(triple7)] The squirrel does not see the cat.[(triple12)] The squirrel is blue.[(triple9)] The squirrel is not rough.[(triple10)] The squirrel is round.[(triple11)] @1: The cat needs the cat.[(((triple3) -> rule3))] The squirrel needs the cat.[(((triple9) -> rule3))] @2: The squirrel is big.[(((((triple9) -> rule3)) -> rule4))] @3: The squirrel is young.[(((((((triple9) -> rule3)) -> rule4)) -> rule1))]
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
triple1
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
triple8
The cat is big.
("cat" "is" "big" "+")
triple2
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat is young.
("cat" "is" "young" "+")
triple6
((triple2) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple7
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
triple12
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple9
The squirrel is not rough.
("squirrel" "is" "rough" "-")
triple10
The squirrel is round.
("squirrel" "is" "round" "+")
triple11
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple3) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
((triple9) -> (rule3 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3