The cow is blue. The cow likes the lion. The cow needs the lion. The cow needs the squirrel. The lion is blue. The lion is cold. The lion is round. The lion likes the squirrel. The lion needs the cow. The lion needs the squirrel. The squirrel is blue. The squirrel likes the lion. The squirrel needs the cow. The squirrel needs the lion. The squirrel visits the cow. The squirrel visits the lion. If something visits the squirrel then it likes the cow. If something is round and blue then it visits the squirrel. If something needs the cow and it is blue then it needs the lion. If something visits the squirrel and it likes the cow then the cow visits the lion. All young things are cold. If something is round then it is young.
The cow is blue.
("cow" "is" "blue" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something visits the squirrel then it likes the cow.
((("something" "visits" "squirrel" "+")) -> ("something" "likes" "cow" "+"))
If something is round and blue then it visits the squirrel.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "visits" "squirrel" "+"))
If something needs the cow and it is blue then it needs the lion.
((("something" "needs" "cow" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "lion" "+"))
If something visits the squirrel and it likes the cow then the cow visits the lion.
((("something" "visits" "squirrel" "+") ("something" "likes" "cow" "+")) -> ("cow" "visits" "lion" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
The squirrel needs the lion.
True
1
proof
[(triple14 OR ((triple13 triple11) -> rule3))]
("squirrel" "needs" "lion" "+")
triple14
((triple13 triple11) -> (rule3 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The cow is not blue.
False
1
inv-proof
[(triple1)]
("cow" "is" "blue" "-")
triple1
The lion is young.
True
2
proof
[(((triple7) -> rule6))]
("lion" "is" "young" "+")
((triple7) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion does not visit the squirrel.
False
3
inv-proof
[(((triple7 triple5) -> rule2))]
("lion" "visits" "squirrel" "-")
((triple7 triple5) -> (rule2 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion likes the cow.
True
4
proof
[(((((triple7 triple5) -> rule2)) -> rule1))]
("lion" "likes" "cow" "+")
((((triple7 triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion does not like the cow.
False
4
inv-proof
[(((((triple7 triple5) -> rule2)) -> rule1))]
("lion" "likes" "cow" "-")
((((triple7 triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The cow visits the lion.
True
8
proof
[(((((triple7 triple5) -> rule2) ((((triple7 triple5) -> rule2)) -> rule1)) -> rule4))]
("cow" "visits" "lion" "+")
((((triple7 triple5) -> (rule2 % int3)) ((((triple7 triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The cow does not visit the lion.
False
8
inv-proof
[(((((triple7 triple5) -> rule2) ((((triple7 triple5) -> rule2)) -> rule1)) -> rule4))]
("cow" "visits" "lion" "-")
((((triple7 triple5) -> (rule2 % int3)) ((((triple7 triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The cow is not cold.
Unknown
inv-rconc
[@2: The cow is cold.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("cow" "is" "cold" "-")
The cow visits the squirrel.
Unknown
rconc
[@1: The cow visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "squirrel" "+")
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "young" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
@0: The cow is blue.[(triple1)] The cow likes the lion.[(triple2)] The cow needs the lion.[(triple3)] The cow needs the squirrel.[(triple4)] The lion is blue.[(triple5)] The lion is cold.[(triple6 OR ((((triple7) -> rule6)) -> rule5))] The lion is round.[(triple7)] The lion likes the squirrel.[(triple8)] The lion needs the cow.[(triple9)] The lion needs the squirrel.[(triple10)] The squirrel is blue.[(triple11)] The squirrel likes the lion.[(triple12)] The squirrel needs the cow.[(triple13)] The squirrel needs the lion.[(triple14 OR ((triple13 triple11) -> rule3))] The squirrel visits the cow.[(triple15)] The squirrel visits the lion.[(triple16)] @1: The lion is young.[(((triple7) -> rule6))] The lion needs the lion.[(((triple9 triple5) -> rule3))] The lion visits the squirrel.[(((triple7 triple5) -> rule2))] @2: The lion likes the cow.[(((((triple7 triple5) -> rule2)) -> rule1))] @3: The cow visits the lion.[(((((triple7 triple5) -> rule2) ((((triple7 triple5) -> rule2)) -> rule1)) -> rule4))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow likes the lion.
("cow" "likes" "lion" "+")
triple2
The cow needs the lion.
("cow" "needs" "lion" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion is cold.
("lion" "is" "cold" "+")
triple6
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is round.
("lion" "is" "round" "+")
triple7
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple8
The lion needs the cow.
("lion" "needs" "cow" "+")
triple9
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple10
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple11
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple12
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple13
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple14
((triple13 triple11) -> (rule3 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple15
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple16
The lion is young.
("lion" "is" "young" "+")
((triple7) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple9 triple5) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((triple7 triple5) -> (rule2 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
((((triple7 triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The cow visits the lion.
("cow" "visits" "lion" "+")
((((triple7 triple5) -> (rule2 % int3)) ((((triple7 triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3