The lion eats the squirrel. The lion is round. The lion needs the squirrel. The lion visits the squirrel. The squirrel eats the lion. The squirrel is big. The squirrel is cold. The squirrel is nice. The squirrel does not need the lion. The squirrel visits the lion. If something needs the lion then it eats the squirrel. If something needs the squirrel and the squirrel eats the lion then it needs the lion. If something is nice then it is cold.
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel does not need the lion.
("squirrel" "needs" "lion" "-")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something needs the lion then it eats the squirrel.
((("something" "needs" "lion" "+")) -> ("something" "eats" "squirrel" "+"))
If something needs the squirrel and the squirrel eats the lion then it needs the lion.
((("something" "needs" "squirrel" "+") ("squirrel" "eats" "lion" "+")) -> ("something" "needs" "lion" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
The squirrel visits the lion.
True
1
proof
[(triple10)]
("squirrel" "visits" "lion" "+")
triple10
The squirrel is not nice.
False
1
inv-proof
[(triple8)]
("squirrel" "is" "nice" "-")
triple8
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "cold" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The lion eats the squirrel.[(triple1 OR ((((triple3 triple5) -> rule2)) -> rule1))] The lion is round.[(triple2)] The lion needs the squirrel.[(triple3)] The lion visits the squirrel.[(triple4)] The squirrel does not need the lion.[(triple9)] The squirrel eats the lion.[(triple5)] The squirrel is big.[(triple6)] The squirrel is cold.[(triple7 OR ((triple8) -> rule3))] The squirrel is nice.[(triple8)] The squirrel visits the lion.[(triple10)] @1: The lion needs the lion.[(((triple3 triple5) -> rule2))]
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple1
((((triple3 triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
triple2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple4
The squirrel does not need the lion.
("squirrel" "needs" "lion" "-")
triple9
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple5
The squirrel is big.
("squirrel" "is" "big" "+")
triple6
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple7
((triple8) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple8
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple10
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple3 triple5) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1