The cat is red. The cat needs the lion. The cat visits the squirrel. The lion is cold. The lion is young. The lion needs the cat. The lion needs the squirrel. The squirrel is cold. The squirrel is rough. The squirrel needs the cat. The squirrel needs the lion. The squirrel visits the cat. If someone is young then they need the squirrel. If the squirrel is red then the squirrel needs the lion. If someone needs the cat and the cat sees the squirrel then the squirrel is rough. If someone visits the lion then the lion needs the squirrel. If someone needs the squirrel then they are red. If someone visits the cat and they are red then they see the squirrel. If someone visits the squirrel then the squirrel is young. If someone is rough and they see the squirrel then they are green.
The cat is red.
("cat" "is" "red" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone is young then they need the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "needs" "squirrel" "+"))
If the squirrel is red then the squirrel needs the lion.
((("squirrel" "is" "red" "+")) -> ("squirrel" "needs" "lion" "+"))
If someone needs the cat and the cat sees the squirrel then the squirrel is rough.
((("someone" "needs" "cat" "+") ("cat" "sees" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If someone visits the lion then the lion needs the squirrel.
((("someone" "visits" "lion" "+")) -> ("lion" "needs" "squirrel" "+"))
If someone needs the squirrel then they are red.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "red" "+"))
If someone visits the cat and they are red then they see the squirrel.
((("someone" "visits" "cat" "+") ("someone" "is" "red" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone visits the squirrel then the squirrel is young.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "is" "young" "+"))
If someone is rough and they see the squirrel then they are green.
((("someone" "is" "rough" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "is" "green" "+"))
The lion is cold.
True
1
proof
[(triple4)]
("lion" "is" "cold" "+")
triple4
The lion is not young.
False
1
inv-proof
[(triple5)]
("lion" "is" "young" "-")
triple5
The squirrel is young.
True
2
proof
[(((triple3) -> rule7))]
("squirrel" "is" "young" "+")
((triple3) -> (rule7 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The lion is not red.
False
2
inv-proof
[(((triple7) -> rule5) OR ((((triple5) -> rule1)) -> rule5))]
("lion" "is" "red" "-")
((triple7) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The squirrel needs the squirrel.
True
3
proof
[(((((triple3) -> rule7)) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel does not need the squirrel.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is red.
True
4
proof
[(((((((triple3) -> rule7)) -> rule1)) -> rule5))]
("squirrel" "is" "red" "+")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The squirrel is not red.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule1)) -> rule5))]
("squirrel" "is" "red" "-")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "green" "-")
The cat sees the squirrel.
Unknown
rconc
[@1: The cat sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "squirrel" "+")
The cat does not need the squirrel.
Unknown
inv-rconc
[@1: The cat needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "squirrel" "-")
The cat is green.
Unknown
rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "green" "+")
The lion does not see the cat.
Unknown
inv-random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The squirrel visits the lion.
Unknown
random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "+")
@0: The cat is red.[(triple1)] The cat needs the lion.[(triple2)] The cat visits the squirrel.[(triple3)] The lion is cold.[(triple4)] The lion is young.[(triple5)] The lion needs the cat.[(triple6)] The lion needs the squirrel.[(triple7 OR ((triple5) -> rule1))] The squirrel is cold.[(triple8)] The squirrel is rough.[(triple9)] The squirrel needs the cat.[(triple10)] The squirrel needs the lion.[(triple11 OR ((((((((triple3) -> rule7)) -> rule1)) -> rule5)) -> rule2))] The squirrel visits the cat.[(triple12)] @1: The lion is red.[(((triple7) -> rule5) OR ((((triple5) -> rule1)) -> rule5))] The squirrel is young.[(((triple3) -> rule7))] @2: The squirrel needs the squirrel.[(((((triple3) -> rule7)) -> rule1))] @3: The squirrel is red.[(((((((triple3) -> rule7)) -> rule1)) -> rule5))] @4: The squirrel sees the squirrel.[(((triple12 ((((((triple3) -> rule7)) -> rule1)) -> rule5)) -> rule6))] @5: The squirrel is green.[(((triple9 ((triple12 ((((((triple3) -> rule7)) -> rule1)) -> rule5)) -> rule6)) -> rule8))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion needs the cat.
("lion" "needs" "cat" "+")
triple6
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple7
((triple5) -> (rule1 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple9
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple10
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple11
((((((((triple3) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int3
The squirrel is young.
("squirrel" "is" "young" "+")
int4
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple12
The lion is red.
("lion" "is" "red" "+")
((triple7) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((triple3) -> (rule7 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple12 ((((((triple3) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int3
The squirrel is young.
("squirrel" "is" "young" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
((triple9 ((triple12 ((((((triple3) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int4
The squirrel is young.
("squirrel" "is" "young" "+")
int5