The cow is cold. The lion is red. The lion is not rough. The lion needs the squirrel. The lion sees the squirrel. The squirrel is cold. The squirrel needs the lion. If someone eats the lion and they do not see the cow then the lion sees the squirrel. If someone is big and rough then they need the cow. If someone eats the cow and the cow is big then they see the squirrel. If someone is nice then they eat the cow. If someone is cold then they eat the cow. If someone is cold and they see the cow then they are nice. If someone is rough then they need the squirrel. If someone eats the cow then they are rough.
The cow is cold.
("cow" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is not rough.
("lion" "is" "rough" "-")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If someone eats the lion and they do not see the cow then the lion sees the squirrel.
((("someone" "eats" "lion" "+") ("someone" "sees" "cow" "~")) -> ("lion" "sees" "squirrel" "+"))
If someone is big and rough then they need the cow.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "needs" "cow" "+"))
If someone eats the cow and the cow is big then they see the squirrel.
((("someone" "eats" "cow" "+") ("cow" "is" "big" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is nice then they eat the cow.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "cow" "+"))
If someone is cold then they eat the cow.
((("someone" "is" "cold" "+")) -> ("someone" "eats" "cow" "+"))
If someone is cold and they see the cow then they are nice.
((("someone" "is" "cold" "+") ("someone" "sees" "cow" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough then they need the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone eats the cow then they are rough.
((("someone" "eats" "cow" "+")) -> ("someone" "is" "rough" "+"))
The squirrel is cold.
True
1
proof
[(triple6)]
("squirrel" "is" "cold" "+")
triple6
The squirrel is not cold.
False
1
inv-proof
[(triple6)]
("squirrel" "is" "cold" "-")
triple6
The cow eats the cow.
True
2
proof
[(((triple1) -> rule5))]
("cow" "eats" "cow" "+")
((triple1) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule5))]
("cow" "eats" "cow" "-")
((triple1) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is rough.
True
3
proof
[(((((triple1) -> rule5)) -> rule8))]
("cow" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is not rough.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule8))]
("cow" "is" "rough" "-")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow needs the squirrel.
True
4
proof
[(((((((triple1) -> rule5)) -> rule8)) -> rule7))]
("cow" "needs" "squirrel" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow does not need the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule8)) -> rule7))]
("cow" "needs" "squirrel" "-")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The lion does not eat the cow.
Unknown
inv-rconc
[@2: The lion eats the cow.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("lion" "eats" "cow" "-")
The cow sees the squirrel.
Unknown
rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "squirrel" "+")
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "cow" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "nice" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The cow sees the lion.
Unknown
random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cow is cold.[(triple1)] The lion is not rough.[(triple3)] The lion is red.[(triple2)] The lion needs the squirrel.[(triple4)] The lion sees the squirrel.[(triple5)] The squirrel is cold.[(triple6)] The squirrel needs the lion.[(triple7)] @1: The cow eats the cow.[(((triple1) -> rule5))] The squirrel eats the cow.[(((triple6) -> rule5))] @2: The cow is rough.[(((((triple1) -> rule5)) -> rule8))] The squirrel is rough.[(((((triple6) -> rule5)) -> rule8))] @3: The cow needs the squirrel.[(((((((triple1) -> rule5)) -> rule8)) -> rule7))] The squirrel needs the squirrel.[(((((((triple6) -> rule5)) -> rule8)) -> rule7))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The lion is not rough.
("lion" "is" "rough" "-")
triple3
The lion is red.
("lion" "is" "red" "+")
triple2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple4
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple5
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple6
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple7
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple1) -> (rule5 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
((triple6) -> (rule5 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3