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