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