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