The lion is cold. The lion is nice. The lion is red. The lion visits the squirrel. The squirrel is cold. The squirrel is green. The squirrel is rough. The squirrel needs the lion. The squirrel sees the lion. The squirrel visits the lion. If something needs the lion and the lion visits the squirrel then it is rough. If something sees the lion then it is green. If something needs the squirrel and it visits the squirrel then the squirrel needs the lion. If something needs the lion then the lion needs the squirrel. If something needs the squirrel then it is rough. If something needs the squirrel then the squirrel sees the lion. If something is green and it sees the lion then it is cold. If something is rough and red then it needs the lion.
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something needs the lion and the lion visits the squirrel then it is rough.
((("something" "needs" "lion" "+") ("lion" "visits" "squirrel" "+")) -> ("something" "is" "rough" "+"))
If something sees the lion then it is green.
((("something" "sees" "lion" "+")) -> ("something" "is" "green" "+"))
If something needs the squirrel and it visits the squirrel then the squirrel needs the lion.
((("something" "needs" "squirrel" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "needs" "lion" "+"))
If something needs the lion then the lion needs the squirrel.
((("something" "needs" "lion" "+")) -> ("lion" "needs" "squirrel" "+"))
If something needs the squirrel then it is rough.
((("something" "needs" "squirrel" "+")) -> ("something" "is" "rough" "+"))
If something needs the squirrel then the squirrel sees the lion.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If something is green and it sees the lion then it is cold.
((("something" "is" "green" "+") ("something" "sees" "lion" "+")) -> ("something" "is" "cold" "+"))
If something is rough and red then it needs the lion.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "needs" "lion" "+"))
The squirrel needs the lion.
True
1
proof
[(triple8)]
("squirrel" "needs" "lion" "+")
triple8
The squirrel is not cold.
False
1
inv-proof
[(triple5 OR ((triple6 triple9) -> rule7) OR ((((triple9) -> rule2) triple9) -> rule7) OR ((triple6 ((((triple8) -> rule4)) -> rule6)) -> rule7) OR ((((triple9) -> rule2) ((((triple8) -> rule4)) -> rule6)) -> rule7) OR ((((((((triple8) -> rule4)) -> rule6)) -> rule2) triple9) -> rule7) OR ((((((((triple8) -> rule4)) -> rule6)) -> rule2) ((((triple8) -> rule4)) -> rule6)) -> rule7))]
("squirrel" "is" "cold" "-")
triple5
((triple6 triple9) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((((triple9) -> (rule2 % int2)) triple9) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
((triple6 ((((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
((((triple9) -> (rule2 % int4)) ((((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
((((((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple9) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int4
((((((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) ((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int4
The lion needs the squirrel.
True
2
proof
[(((triple8) -> rule4))]
("lion" "needs" "squirrel" "+")
((triple8) -> (rule4 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion does not need the squirrel.
False
2
inv-proof
[(((triple8) -> rule4))]
("lion" "needs" "squirrel" "-")
((triple8) -> (rule4 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion is rough.
True
3
proof
[(((((triple8) -> rule4)) -> rule5))]
("lion" "is" "rough" "+")
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion is not rough.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule5))]
("lion" "is" "rough" "-")
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion needs the lion.
True
5
proof
[(((((((triple8) -> rule4)) -> rule5) triple3) -> rule8))]
("lion" "needs" "lion" "+")
((((((triple8) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The lion does not need the lion.
False
5
inv-proof
[(((((((triple8) -> rule4)) -> rule5) triple3) -> rule8))]
("lion" "needs" "lion" "-")
((((((triple8) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "green" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "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 squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The lion does not see the squirrel.
Unknown
inv-random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
@0: The lion is cold.[(triple1)] The lion is nice.[(triple2)] The lion is red.[(triple3)] The lion visits the squirrel.[(triple4)] The squirrel is cold.[(triple5 OR ((triple6 triple9) -> rule7) OR ((((triple9) -> rule2) triple9) -> rule7) OR ((triple6 ((((triple8) -> rule4)) -> rule6)) -> rule7) OR ((((triple9) -> rule2) ((((triple8) -> rule4)) -> rule6)) -> rule7) OR ((((((((triple8) -> rule4)) -> rule6)) -> rule2) triple9) -> rule7) OR ((((((((triple8) -> rule4)) -> rule6)) -> rule2) ((((triple8) -> rule4)) -> rule6)) -> rule7))] The squirrel is green.[(triple6 OR ((triple9) -> rule2) OR ((((((triple8) -> rule4)) -> rule6)) -> rule2))] The squirrel is rough.[(triple7 OR ((triple8 triple4) -> rule1))] The squirrel needs the lion.[(triple8)] The squirrel sees the lion.[(triple9 OR ((((triple8) -> rule4)) -> rule6))] The squirrel visits the lion.[(triple10)] @1: The lion needs the squirrel.[(((triple8) -> rule4))] @2: The lion is rough.[(((((triple8) -> rule4)) -> rule5))] @3: The lion needs the lion.[(((((((triple8) -> rule4)) -> rule5) triple3) -> rule8))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple4
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple5
((triple6 triple9) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((((triple9) -> (rule2 % int2)) triple9) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
((triple6 ((((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
((((triple9) -> (rule2 % int4)) ((((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
((((((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple9) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int4
((((((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) ((((triple8) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int4
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
((triple9) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((((((triple8) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple7
((triple8 triple4) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple8
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple9
((((triple8) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple10
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
((triple8) -> (rule4 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
((((((triple8) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3