The lion is red. The squirrel eats the lion. If the lion is red and the lion eats the squirrel then the lion visits the squirrel. If something is nice and it chases the squirrel then the squirrel visits the lion. If something visits the squirrel then it is big. If something eats the lion then the lion is nice. If something eats the lion then the lion eats the squirrel. Rough things are cold.
The lion is red.
("lion" "is" "red" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
If the lion is red and the lion eats the squirrel then the lion visits the squirrel.
((("lion" "is" "red" "+") ("lion" "eats" "squirrel" "+")) -> ("lion" "visits" "squirrel" "+"))
If something is nice and it chases the squirrel then the squirrel visits the lion.
((("something" "is" "nice" "+") ("something" "chases" "squirrel" "+")) -> ("squirrel" "visits" "lion" "+"))
If something visits the squirrel then it is big.
((("something" "visits" "squirrel" "+")) -> ("something" "is" "big" "+"))
If something eats the lion then the lion is nice.
((("something" "eats" "lion" "+")) -> ("lion" "is" "nice" "+"))
If something eats the lion then the lion eats the squirrel.
((("something" "eats" "lion" "+")) -> ("lion" "eats" "squirrel" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
The squirrel eats the lion.
True
1
proof
[(triple2)]
("squirrel" "eats" "lion" "+")
triple2
The lion is not red.
False
1
inv-proof
[(triple1)]
("lion" "is" "red" "-")
triple1
The lion eats the squirrel.
True
2
proof
[(((triple2) -> rule5))]
("lion" "eats" "squirrel" "+")
((triple2) -> (rule5 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion is not nice.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "is" "nice" "-")
((triple2) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion visits the squirrel.
True
4
proof
[(((triple1 ((triple2) -> rule5)) -> rule1))]
("lion" "visits" "squirrel" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion does not visit the squirrel.
False
4
inv-proof
[(((triple1 ((triple2) -> rule5)) -> rule1))]
("lion" "visits" "squirrel" "-")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion is big.
True
5
proof
[(((((triple1 ((triple2) -> rule5)) -> rule1)) -> rule3))]
("lion" "is" "big" "+")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int3
The lion is not big.
False
5
inv-proof
[(((((triple1 ((triple2) -> rule5)) -> rule1)) -> rule3))]
("lion" "is" "big" "-")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int3
The squirrel is not big.
Unknown
inv-rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "big" "-")
The squirrel visits the lion.
Unknown
rconc
[@1: The squirrel visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "lion" "+")
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "cold" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "cold" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The lion does not chase the squirrel.
Unknown
inv-random
[@0: The lion chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The lion is red.[(triple1)] The squirrel eats the lion.[(triple2)] @1: The lion eats the squirrel.[(((triple2) -> rule5))] The lion is nice.[(((triple2) -> rule4))] @2: The lion visits the squirrel.[(((triple1 ((triple2) -> rule5)) -> rule1))] @3: The lion is big.[(((((triple1 ((triple2) -> rule5)) -> rule1)) -> rule3))]
The lion is red.
("lion" "is" "red" "+")
triple1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple2
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
((triple2) -> (rule5 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((triple2) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int3