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