The bear sees the lion. The cow chases the lion. The cow is kind. The cow is nice. The cow sees the lion. The lion chases the cow. The lion is not red. The squirrel is not nice. The squirrel is red. The squirrel needs the cow. The squirrel needs the lion. If the bear is blue and the bear sees the lion then the lion does not see the bear. If the bear is kind and the bear is nice then the bear does not see the cow. If something is blue and it chases the bear then it sees the cow. If something is nice and it needs the cow then it is kind. If something is cold then it needs the lion. If something needs the lion then it needs the bear. If something is blue and not kind then it is cold. If something sees the squirrel then it is cold. If something needs the bear then the bear sees the squirrel.
The bear sees the lion.
("bear" "sees" "lion" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is not red.
("lion" "is" "red" "-")
The squirrel is not nice.
("squirrel" "is" "nice" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If the bear is blue and the bear sees the lion then the lion does not see the bear.
((("bear" "is" "blue" "+") ("bear" "sees" "lion" "+")) -> ("lion" "sees" "bear" "-"))
If the bear is kind and the bear is nice then the bear does not see the cow.
((("bear" "is" "kind" "+") ("bear" "is" "nice" "+")) -> ("bear" "sees" "cow" "-"))
If something is blue and it chases the bear then it sees the cow.
((("something" "is" "blue" "+") ("something" "chases" "bear" "+")) -> ("something" "sees" "cow" "+"))
If something is nice and it needs the cow then it is kind.
((("something" "is" "nice" "+") ("something" "needs" "cow" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it needs the lion.
((("something" "is" "cold" "+")) -> ("something" "needs" "lion" "+"))
If something needs the lion then it needs the bear.
((("something" "needs" "lion" "+")) -> ("something" "needs" "bear" "+"))
If something is blue and not kind then it is cold.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "cold" "+"))
If something sees the squirrel then it is cold.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "cold" "+"))
If something needs the bear then the bear sees the squirrel.
((("something" "needs" "bear" "+")) -> ("bear" "sees" "squirrel" "+"))
The squirrel is red.
True
1
proof
[(triple9)]
("squirrel" "is" "red" "+")
triple9
The cow is not kind.
False
1
inv-proof
[(triple3)]
("cow" "is" "kind" "-")
triple3
The squirrel needs the bear.
True
2
proof
[(((triple11) -> rule6))]
("squirrel" "needs" "bear" "+")
((triple11) -> (rule6 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel does not need the bear.
False
2
inv-proof
[(((triple11) -> rule6))]
("squirrel" "needs" "bear" "-")
((triple11) -> (rule6 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The bear sees the squirrel.
True
3
proof
[(((((triple11) -> rule6)) -> rule9))]
("bear" "sees" "squirrel" "+")
((((triple11) -> (rule6 % int2))) -> (rule9 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The bear does not see the squirrel.
False
3
inv-proof
[(((((triple11) -> rule6)) -> rule9))]
("bear" "sees" "squirrel" "-")
((((triple11) -> (rule6 % int2))) -> (rule9 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The bear is cold.
True
4
proof
[(((((((triple11) -> rule6)) -> rule9)) -> rule8))]
("bear" "is" "cold" "+")
((((((triple11) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
The bear is not cold.
False
4
inv-proof
[(((((((triple11) -> rule6)) -> rule9)) -> rule8))]
("bear" "is" "cold" "-")
((((((triple11) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
The bear needs the lion.
True
5
proof
[(((((((((triple11) -> rule6)) -> rule9)) -> rule8)) -> rule5))]
("bear" "needs" "lion" "+")
((((((((triple11) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int4
The bear does not need the lion.
False
5
inv-proof
[(((((((((triple11) -> rule6)) -> rule9)) -> rule8)) -> rule5))]
("bear" "needs" "lion" "-")
((((((((triple11) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int4
The bear needs the bear.
True
6
proof
[(((((((((((triple11) -> rule6)) -> rule9)) -> rule8)) -> rule5)) -> rule6))]
("bear" "needs" "bear" "+")
((((((((((triple11) -> (rule6 % int5))) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int4
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int5
The bear does not need the bear.
False
6
inv-proof
[(((((((((((triple11) -> rule6)) -> rule9)) -> rule8)) -> rule5)) -> rule6))]
("bear" "needs" "bear" "-")
((((((((((triple11) -> (rule6 % int5))) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int4
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int5
The squirrel is not kind.
Unknown
inv-rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "kind" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "cold" "+")
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "cold" "-")
The bear sees the cow.
Unknown
rconc
[@1: The bear sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "cow" "+")
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "kind" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "is" "cold" "+")
The squirrel does not chase the cow.
Unknown
inv-random
[@0: The squirrel chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow does not need the squirrel.
Unknown
inv-random
[@0: The cow needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "squirrel" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The cow sees the bear.
Unknown
random
[@0: The cow sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "bear" "+")
@0: The bear sees the lion.[(triple1)] The cow chases the lion.[(triple2)] The cow is kind.[(triple3)] The cow is nice.[(triple4)] The cow sees the lion.[(triple5)] The lion chases the cow.[(triple6)] The lion is not red.[(triple7)] The squirrel is not nice.[(triple8)] The squirrel is red.[(triple9)] The squirrel needs the cow.[(triple10)] The squirrel needs the lion.[(triple11)] @1: The squirrel needs the bear.[(((triple11) -> rule6))] @2: The bear sees the squirrel.[(((((triple11) -> rule6)) -> rule9))] @3: The bear is cold.[(((((((triple11) -> rule6)) -> rule9)) -> rule8))] @4: The bear needs the lion.[(((((((((triple11) -> rule6)) -> rule9)) -> rule8)) -> rule5))] @5: The bear needs the bear.[(((((((((((triple11) -> rule6)) -> rule9)) -> rule8)) -> rule5)) -> rule6))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The cow chases the lion.
("cow" "chases" "lion" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow sees the lion.
("cow" "sees" "lion" "+")
triple5
The lion chases the cow.
("lion" "chases" "cow" "+")
triple6
The lion is not red.
("lion" "is" "red" "-")
triple7
The squirrel is not nice.
("squirrel" "is" "nice" "-")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple10
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple11
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
((triple11) -> (rule6 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((((triple11) -> (rule6 % int2))) -> (rule9 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
((((((triple11) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int3
The bear needs the lion.
("bear" "needs" "lion" "+")
((((((((triple11) -> (rule6 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
((((((((((triple11) -> (rule6 % int5))) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int4
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int5