The cat visits the lion. The lion is green. The lion is young. The lion sees the squirrel. The squirrel eats the cat. The squirrel sees the cat. The squirrel sees the lion. If someone is green and rough then they eat the cat. If someone sees the lion then they are round. If someone is round and they see the lion then the lion is rough. If someone sees the squirrel then the squirrel visits the cat. If someone visits the squirrel then they visit the lion. If someone visits the squirrel then they are young.
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If someone is green and rough then they eat the cat.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "eats" "cat" "+"))
If someone sees the lion then they are round.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "round" "+"))
If someone is round and they see the lion then the lion is rough.
((("someone" "is" "round" "+") ("someone" "sees" "lion" "+")) -> ("lion" "is" "rough" "+"))
If someone sees the squirrel then the squirrel visits the cat.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "visits" "cat" "+"))
If someone visits the squirrel then they visit the lion.
((("someone" "visits" "squirrel" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the squirrel then they are young.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "young" "+"))
The squirrel sees the cat.
True
1
proof
[(triple6)]
("squirrel" "sees" "cat" "+")
triple6
The lion is not young.
False
1
inv-proof
[(triple3)]
("lion" "is" "young" "-")
triple3
The squirrel is round.
True
2
proof
[(((triple7) -> rule2))]
("squirrel" "is" "round" "+")
((triple7) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel does not visit the cat.
False
2
inv-proof
[(((triple4) -> rule4))]
("squirrel" "visits" "cat" "-")
((triple4) -> (rule4 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The lion is rough.
True
4
proof
[(((((triple7) -> rule2) triple7) -> rule3))]
("lion" "is" "rough" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The lion is not rough.
False
4
inv-proof
[(((((triple7) -> rule2) triple7) -> rule3))]
("lion" "is" "rough" "-")
((((triple7) -> (rule2 % int2)) triple7) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The lion eats the cat.
True
6
proof
[(((triple2 ((((triple7) -> rule2) triple7) -> rule3)) -> rule1))]
("lion" "eats" "cat" "+")
((triple2 ((((triple7) -> (rule2 % int3)) triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The lion does not eat the cat.
False
6
inv-proof
[(((triple2 ((((triple7) -> rule2) triple7) -> rule3)) -> rule1))]
("lion" "eats" "cat" "-")
((triple2 ((((triple7) -> (rule2 % int3)) triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "young" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "round" "+")
The squirrel does not visit the lion.
Unknown
inv-rconc
[@1: The squirrel visits the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "visits" "lion" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "round" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The lion visits the cat.
Unknown
random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "+")
The cat does not visit the squirrel.
Unknown
inv-random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "-")
The lion visits the squirrel.
Unknown
random
[@0: The lion visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "squirrel" "+")
@0: The cat visits the lion.[(triple1)] The lion is green.[(triple2)] The lion is young.[(triple3)] The lion sees the squirrel.[(triple4)] The squirrel eats the cat.[(triple5)] The squirrel sees the cat.[(triple6)] The squirrel sees the lion.[(triple7)] @1: The squirrel is round.[(((triple7) -> rule2))] The squirrel visits the cat.[(((triple4) -> rule4))] @2: The lion is rough.[(((((triple7) -> rule2) triple7) -> rule3))] @3: The lion eats the cat.[(((triple2 ((((triple7) -> rule2) triple7) -> rule3)) -> rule1))]
The cat visits the lion.
("cat" "visits" "lion" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple4
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple5
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple6
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple7
The squirrel is round.
("squirrel" "is" "round" "+")
((triple7) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple4) -> (rule4 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
((triple2 ((((triple7) -> (rule2 % int3)) triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3