The bear is blue. The bear is nice. The bear likes the cat. The bear likes the squirrel. The bear visits the squirrel. The bear visits the tiger. The cat is blue. The cat is red. The cat likes the tiger. The cat visits the bear. The squirrel is blue. The tiger is blue. The tiger is nice. The tiger visits the bear. If something likes the bear then the bear needs the tiger. If something is red then it likes the bear. If the squirrel is nice and the squirrel visits the cat then the squirrel visits the tiger. Young things are red. If the squirrel likes the cat and the cat needs the squirrel then the squirrel is nice. If something visits the cat then the cat is nice. If something needs the tiger then it is young. If something likes the squirrel and it needs the bear then it needs the tiger.
The bear is blue.
("bear" "is" "blue" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something likes the bear then the bear needs the tiger.
((("something" "likes" "bear" "+")) -> ("bear" "needs" "tiger" "+"))
If something is red then it likes the bear.
((("something" "is" "red" "+")) -> ("something" "likes" "bear" "+"))
If the squirrel is nice and the squirrel visits the cat then the squirrel visits the tiger.
((("squirrel" "is" "nice" "+") ("squirrel" "visits" "cat" "+")) -> ("squirrel" "visits" "tiger" "+"))
Young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If the squirrel likes the cat and the cat needs the squirrel then the squirrel is nice.
((("squirrel" "likes" "cat" "+") ("cat" "needs" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If something visits the cat then the cat is nice.
((("something" "visits" "cat" "+")) -> ("cat" "is" "nice" "+"))
If something needs the tiger then it is young.
((("something" "needs" "tiger" "+")) -> ("something" "is" "young" "+"))
If something likes the squirrel and it needs the bear then it needs the tiger.
((("something" "likes" "squirrel" "+") ("something" "needs" "bear" "+")) -> ("something" "needs" "tiger" "+"))
The bear visits the squirrel.
True
1
proof
[(triple5)]
("bear" "visits" "squirrel" "+")
triple5
The cat is not blue.
False
1
inv-proof
[(triple7)]
("cat" "is" "blue" "-")
triple7
The cat likes the bear.
True
2
proof
[(((triple8) -> rule2))]
("cat" "likes" "bear" "+")
((triple8) -> (rule2 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The cat does not like the bear.
False
2
inv-proof
[(((triple8) -> rule2))]
("cat" "likes" "bear" "-")
((triple8) -> (rule2 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear needs the tiger.
True
3
proof
[(((((triple8) -> rule2)) -> rule1))]
("bear" "needs" "tiger" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear does not need the tiger.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule1))]
("bear" "needs" "tiger" "-")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear is young.
True
4
proof
[(((((((triple8) -> rule2)) -> rule1)) -> rule7))]
("bear" "is" "young" "+")
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3
The bear is not young.
False
4
inv-proof
[(((((((triple8) -> rule2)) -> rule1)) -> rule7))]
("bear" "is" "young" "-")
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3
The bear is red.
True
5
proof
[(((((((((triple8) -> rule2)) -> rule1)) -> rule7)) -> rule4))]
("bear" "is" "red" "+")
((((((((triple8) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The cat likes the bear.
("cat" "likes" "bear" "+")
int4
The bear is not red.
False
5
inv-proof
[(((((((((triple8) -> rule2)) -> rule1)) -> rule7)) -> rule4))]
("bear" "is" "red" "-")
((((((((triple8) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The cat likes the bear.
("cat" "likes" "bear" "+")
int4
The bear likes the bear.
True
6
proof
[(((((((((((triple8) -> rule2)) -> rule1)) -> rule7)) -> rule4)) -> rule2))]
("bear" "likes" "bear" "+")
((((((((((triple8) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int4
The cat likes the bear.
("cat" "likes" "bear" "+")
int5
The bear does not like the bear.
False
6
inv-proof
[(((((((((((triple8) -> rule2)) -> rule1)) -> rule7)) -> rule4)) -> rule2))]
("bear" "likes" "bear" "-")
((((((((((triple8) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int4
The cat likes the bear.
("cat" "likes" "bear" "+")
int5
The squirrel does not need the tiger.
Unknown
inv-rconc
[@1: The squirrel needs the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "needs" "tiger" "-")
The cat needs the tiger.
Unknown
rconc
[@1: The cat needs the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "needs" "tiger" "+")
The squirrel does not like the bear.
Unknown
inv-rconc
[@4: The squirrel likes the bear.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule7 <- rule8 <- FAIL)]]
("squirrel" "likes" "bear" "-")
The squirrel is young.
Unknown
rconc
[@2: The squirrel is young.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("squirrel" "is" "young" "+")
The tiger does not like the bear.
Unknown
inv-rconc
[@4: The tiger likes the bear.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule7 <- rule8 <- FAIL)]]
("tiger" "likes" "bear" "-")
The squirrel visits the tiger.
Unknown
rconc
[@1: The squirrel visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "tiger" "+")
The bear does not like the tiger.
Unknown
inv-random
[@0: The bear likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The tiger does not visit the cat.
Unknown
inv-random
[@0: The tiger visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The bear is blue.[(triple1)] The bear is nice.[(triple2)] The bear likes the cat.[(triple3)] The bear likes the squirrel.[(triple4)] The bear visits the squirrel.[(triple5)] The bear visits the tiger.[(triple6)] The cat is blue.[(triple7)] The cat is red.[(triple8)] The cat likes the tiger.[(triple9)] The cat visits the bear.[(triple10)] The squirrel is blue.[(triple11)] The tiger is blue.[(triple12)] The tiger is nice.[(triple13)] The tiger visits the bear.[(triple14)] @1: The cat likes the bear.[(((triple8) -> rule2))] @2: The bear needs the tiger.[(((((triple8) -> rule2)) -> rule1))] @3: The bear is young.[(((((((triple8) -> rule2)) -> rule1)) -> rule7))] @4: The bear is red.[(((((((((triple8) -> rule2)) -> rule1)) -> rule7)) -> rule4))] @5: The bear likes the bear.[(((((((((((triple8) -> rule2)) -> rule1)) -> rule7)) -> rule4)) -> rule2))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear likes the cat.
("bear" "likes" "cat" "+")
triple3
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple4
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple5
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple6
The cat is blue.
("cat" "is" "blue" "+")
triple7
The cat is red.
("cat" "is" "red" "+")
triple8
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple9
The cat visits the bear.
("cat" "visits" "bear" "+")
triple10
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple11
The tiger is blue.
("tiger" "is" "blue" "+")
triple12
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple14
The cat likes the bear.
("cat" "likes" "bear" "+")
((triple8) -> (rule2 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear is young.
("bear" "is" "young" "+")
((((((triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3
The bear is red.
("bear" "is" "red" "+")
((((((((triple8) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The cat likes the bear.
("cat" "likes" "bear" "+")
int4
The bear likes the bear.
("bear" "likes" "bear" "+")
((((((((((triple8) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int4
The cat likes the bear.
("cat" "likes" "bear" "+")
int5