The squirrel is big. The squirrel is nice. The squirrel is red. The squirrel is rough. The squirrel is young. The squirrel does not like the tiger. The squirrel needs the tiger. The squirrel sees the tiger. The tiger is big. The tiger likes the squirrel. The tiger does not need the squirrel. The tiger sees the squirrel. If something likes the squirrel then it is red. If something needs the squirrel and the squirrel sees the tiger then it sees the squirrel. If something likes the squirrel then it needs the tiger. If something likes the squirrel and it sees the squirrel then the squirrel needs the tiger. If something sees the squirrel then the squirrel is nice. If something sees the tiger and the tiger is red then it needs the squirrel. If something likes the tiger and it is not big then it is young. If something likes the tiger then it does not like the squirrel.
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something likes the squirrel then it is red.
((("something" "likes" "squirrel" "+")) -> ("something" "is" "red" "+"))
If something needs the squirrel and the squirrel sees the tiger then it sees the squirrel.
((("something" "needs" "squirrel" "+") ("squirrel" "sees" "tiger" "+")) -> ("something" "sees" "squirrel" "+"))
If something likes the squirrel then it needs the tiger.
((("something" "likes" "squirrel" "+")) -> ("something" "needs" "tiger" "+"))
If something likes the squirrel and it sees the squirrel then the squirrel needs the tiger.
((("something" "likes" "squirrel" "+") ("something" "sees" "squirrel" "+")) -> ("squirrel" "needs" "tiger" "+"))
If something sees the squirrel then the squirrel is nice.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If something sees the tiger and the tiger is red then it needs the squirrel.
((("something" "sees" "tiger" "+") ("tiger" "is" "red" "+")) -> ("something" "needs" "squirrel" "+"))
If something likes the tiger and it is not big then it is young.
((("something" "likes" "tiger" "+") ("something" "is" "big" "~")) -> ("something" "is" "young" "+"))
If something likes the tiger then it does not like the squirrel.
((("something" "likes" "tiger" "+")) -> ("something" "likes" "squirrel" "-"))
The squirrel does not like the tiger.
True
1
proof
[(triple6)]
("squirrel" "likes" "tiger" "-")
triple6
The tiger needs the squirrel.
False
1
inv-proof
[(triple11)]
("tiger" "needs" "squirrel" "+")
triple11
The tiger is red.
True
2
proof
[(((triple10) -> rule1))]
("tiger" "is" "red" "+")
((triple10) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger does not need the tiger.
False
2
inv-proof
[(((triple10) -> rule3))]
("tiger" "needs" "tiger" "-")
((triple10) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The squirrel needs the squirrel.
True
4
proof
[(((triple8 ((triple10) -> rule1)) -> rule6))]
("squirrel" "needs" "squirrel" "+")
((triple8 ((triple10) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The squirrel does not need the squirrel.
False
4
inv-proof
[(((triple8 ((triple10) -> rule1)) -> rule6))]
("squirrel" "needs" "squirrel" "-")
((triple8 ((triple10) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The squirrel sees the squirrel.
True
6
proof
[(((((triple8 ((triple10) -> rule1)) -> rule6) triple8) -> rule2))]
("squirrel" "sees" "squirrel" "+")
((((triple8 ((triple10) -> (rule1 % int3))) -> (rule6 % int2)) triple8) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The squirrel does not see the squirrel.
False
6
inv-proof
[(((((triple8 ((triple10) -> rule1)) -> rule6) triple8) -> rule2))]
("squirrel" "sees" "squirrel" "-")
((((triple8 ((triple10) -> (rule1 % int3))) -> (rule6 % int2)) triple8) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "young" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The squirrel does not like the tiger.[(triple6)] The squirrel is big.[(triple1)] The squirrel is nice.[(triple2 OR ((triple12) -> rule5) OR ((((((triple8 ((triple10) -> rule1)) -> rule6) triple8) -> rule2)) -> rule5))] The squirrel is red.[(triple3)] The squirrel is rough.[(triple4)] The squirrel is young.[(triple5)] The squirrel needs the tiger.[(triple7 OR ((triple10 triple12) -> rule4))] The squirrel sees the tiger.[(triple8)] The tiger does not need the squirrel.[(triple11)] The tiger is big.[(triple9)] The tiger likes the squirrel.[(triple10)] The tiger sees the squirrel.[(triple12)] @1: The tiger is red.[(((triple10) -> rule1))] The tiger needs the tiger.[(((triple10) -> rule3))] @2: The squirrel needs the squirrel.[(((triple8 ((triple10) -> rule1)) -> rule6))] @3: The squirrel sees the squirrel.[(((((triple8 ((triple10) -> rule1)) -> rule6) triple8) -> rule2))]
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple2
((triple12) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((((((triple8 ((triple10) -> (rule1 % int4))) -> (rule6 % int3)) triple8) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple4
The squirrel is young.
("squirrel" "is" "young" "+")
triple5
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple7
((triple10 triple12) -> (rule4 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple8
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple11
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple10
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
((triple10) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple10) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple8 ((triple10) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple8 ((triple10) -> (rule1 % int3))) -> (rule6 % int2)) triple8) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3