The bear is young. The cow likes the bear. The cow sees the squirrel. The lion is cold. The lion is nice. The lion sees the cow. The squirrel needs the lion. If someone is nice then they like the cow. If someone likes the lion then they like the squirrel. If someone likes the bear then the bear likes the lion. If someone likes the cow and the cow likes the bear then they see the squirrel. If the lion sees the squirrel then the squirrel is nice. If the cow is cold then the cow sees the lion.
The bear is young.
("bear" "is" "young" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If someone is nice then they like the cow.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the lion then they like the squirrel.
((("someone" "likes" "lion" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone likes the bear then the bear likes the lion.
((("someone" "likes" "bear" "+")) -> ("bear" "likes" "lion" "+"))
If someone likes the cow and the cow likes the bear then they see the squirrel.
((("someone" "likes" "cow" "+") ("cow" "likes" "bear" "+")) -> ("someone" "sees" "squirrel" "+"))
If the lion sees the squirrel then the squirrel is nice.
((("lion" "sees" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If the cow is cold then the cow sees the lion.
((("cow" "is" "cold" "+")) -> ("cow" "sees" "lion" "+"))
The bear is young.
True
1
proof
[(triple1)]
("bear" "is" "young" "+")
triple1
The cow does not like the bear.
False
1
inv-proof
[(triple2)]
("cow" "likes" "bear" "-")
triple2
The lion likes the cow.
True
2
proof
[(((triple5) -> rule1))]
("lion" "likes" "cow" "+")
((triple5) -> (rule1 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion does not like the cow.
False
2
inv-proof
[(((triple5) -> rule1))]
("lion" "likes" "cow" "-")
((triple5) -> (rule1 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion sees the squirrel.
True
4
proof
[(((((triple5) -> rule1) triple2) -> rule4))]
("lion" "sees" "squirrel" "+")
((((triple5) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion does not see the squirrel.
False
4
inv-proof
[(((((triple5) -> rule1) triple2) -> rule4))]
("lion" "sees" "squirrel" "-")
((((triple5) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The squirrel is nice.
True
5
proof
[(((((((triple5) -> rule1) triple2) -> rule4)) -> rule5))]
("squirrel" "is" "nice" "+")
((((((triple5) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion likes the cow.
("lion" "likes" "cow" "+")
int3
The squirrel is not nice.
False
5
inv-proof
[(((((((triple5) -> rule1) triple2) -> rule4)) -> rule5))]
("squirrel" "is" "nice" "-")
((((((triple5) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion likes the cow.
("lion" "likes" "cow" "+")
int3
The squirrel likes the cow.
True
6
proof
[(((((((((triple5) -> rule1) triple2) -> rule4)) -> rule5)) -> rule1))]
("squirrel" "likes" "cow" "+")
((((((((triple5) -> (rule1 % int4)) triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3
The lion likes the cow.
("lion" "likes" "cow" "+")
int4
The squirrel does not like the cow.
False
6
inv-proof
[(((((((((triple5) -> rule1) triple2) -> rule4)) -> rule5)) -> rule1))]
("squirrel" "likes" "cow" "-")
((((((((triple5) -> (rule1 % int4)) triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3
The lion likes the cow.
("lion" "likes" "cow" "+")
int4
The squirrel sees the squirrel.
True
8
proof
[(((((((((((triple5) -> rule1) triple2) -> rule4)) -> rule5)) -> rule1) triple2) -> rule4))]
("squirrel" "sees" "squirrel" "+")
((((((((((triple5) -> (rule1 % int5)) triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int4
The lion likes the cow.
("lion" "likes" "cow" "+")
int5
The squirrel does not see the squirrel.
False
8
inv-proof
[(((((((((((triple5) -> rule1) triple2) -> rule4)) -> rule5)) -> rule1) triple2) -> rule4))]
("squirrel" "sees" "squirrel" "-")
((((((((((triple5) -> (rule1 % int5)) triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int4
The lion likes the cow.
("lion" "likes" "cow" "+")
int5
The lion does not like the squirrel.
Unknown
inv-rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "squirrel" "-")
The cow sees the lion.
Unknown
rconc
[@1: The cow sees the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "sees" "lion" "+")
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The bear likes the cow.
Unknown
rconc
[@1: The bear likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "cow" "+")
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cow" "-")
The bear sees the squirrel.
Unknown
rconc
[@2: The bear sees the squirrel.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("bear" "sees" "squirrel" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The bear sees the cow.
Unknown
random
[@0: The bear sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cow" "+")
The bear does not need the lion.
Unknown
inv-random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The bear is young.[(triple1)] The cow likes the bear.[(triple2)] The cow sees the squirrel.[(triple3)] The lion is cold.[(triple4)] The lion is nice.[(triple5)] The lion sees the cow.[(triple6)] The squirrel needs the lion.[(triple7)] @1: The bear likes the lion.[(((triple2) -> rule3))] The lion likes the cow.[(((triple5) -> rule1))] @2: The bear likes the squirrel.[(((((triple2) -> rule3)) -> rule2))] The lion sees the squirrel.[(((((triple5) -> rule1) triple2) -> rule4))] @3: The squirrel is nice.[(((((((triple5) -> rule1) triple2) -> rule4)) -> rule5))] @4: The squirrel likes the cow.[(((((((((triple5) -> rule1) triple2) -> rule4)) -> rule5)) -> rule1))] @5: The squirrel sees the squirrel.[(((((((((((triple5) -> rule1) triple2) -> rule4)) -> rule5)) -> rule1) triple2) -> rule4))]
The bear is young.
("bear" "is" "young" "+")
triple1
The cow likes the bear.
("cow" "likes" "bear" "+")
triple2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion is nice.
("lion" "is" "nice" "+")
triple5
The lion sees the cow.
("lion" "sees" "cow" "+")
triple6
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple7
The bear likes the lion.
("bear" "likes" "lion" "+")
((triple2) -> (rule3 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
((triple5) -> (rule1 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear likes the lion.
("bear" "likes" "lion" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((triple5) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((((triple5) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The lion likes the cow.
("lion" "likes" "cow" "+")
int3
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((((((((triple5) -> (rule1 % int4)) triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int3
The lion likes the cow.
("lion" "likes" "cow" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((((((((triple5) -> (rule1 % int5)) triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int4
The lion likes the cow.
("lion" "likes" "cow" "+")
int5