The cow is cold. The cow is young. The cow likes the lion. The cow sees the lion. The lion is cold. The lion is red. The lion needs the cow. If something is red then it is blue. If something likes the lion and the lion sees the cow then it sees the cow. If something is cold and blue then it sees the cow. If the cow needs the lion and the lion likes the cow then the cow likes the lion. If something sees the lion then it is red. If something needs the cow and the cow is big then the cow likes the lion. If something needs the cow then it is cold. If something needs the cow then the cow sees the lion.
The cow is cold.
("cow" "is" "cold" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something likes the lion and the lion sees the cow then it sees the cow.
((("something" "likes" "lion" "+") ("lion" "sees" "cow" "+")) -> ("something" "sees" "cow" "+"))
If something is cold and blue then it sees the cow.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "sees" "cow" "+"))
If the cow needs the lion and the lion likes the cow then the cow likes the lion.
((("cow" "needs" "lion" "+") ("lion" "likes" "cow" "+")) -> ("cow" "likes" "lion" "+"))
If something sees the lion then it is red.
((("something" "sees" "lion" "+")) -> ("something" "is" "red" "+"))
If something needs the cow and the cow is big then the cow likes the lion.
((("something" "needs" "cow" "+") ("cow" "is" "big" "+")) -> ("cow" "likes" "lion" "+"))
If something needs the cow then it is cold.
((("something" "needs" "cow" "+")) -> ("something" "is" "cold" "+"))
If something needs the cow then the cow sees the lion.
((("something" "needs" "cow" "+")) -> ("cow" "sees" "lion" "+"))
The cow sees the lion.
True
1
proof
[(triple4 OR ((triple7) -> rule8))]
("cow" "sees" "lion" "+")
triple4
((triple7) -> (rule8 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The lion is not cold.
False
1
inv-proof
[(triple5 OR ((triple7) -> rule7))]
("lion" "is" "cold" "-")
triple5
((triple7) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is blue.
True
2
proof
[(((triple6) -> rule1))]
("lion" "is" "blue" "+")
((triple6) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The cow is not red.
False
2
inv-proof
[(((triple4) -> rule5) OR ((((triple7) -> rule8)) -> rule5))]
("cow" "is" "red" "-")
((triple4) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
int2
The cow is blue.
True
3
proof
[(((((triple4) -> rule5)) -> rule1) OR ((((((triple7) -> rule8)) -> rule5)) -> rule1))]
("cow" "is" "blue" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((((triple7) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow sees the lion.
("cow" "sees" "lion" "+")
int3
The lion does not see the cow.
False
4
inv-proof
[(((triple5 ((triple6) -> rule1)) -> rule3) OR ((((triple7) -> rule7) ((triple6) -> rule1)) -> rule3))]
("lion" "sees" "cow" "-")
((triple5 ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple7) -> (rule7 % int3)) ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The cow sees the cow.
True
5
proof
[(((triple1 ((((triple4) -> rule5)) -> rule1)) -> rule3) OR ((triple3 ((triple5 ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((triple3 ((((triple7) -> rule7) ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((triple1 ((((((triple7) -> rule8)) -> rule5)) -> rule1)) -> rule3))]
("cow" "sees" "cow" "+")
((triple1 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
((triple3 ((triple5 ((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((triple3 ((((triple7) -> (rule7 % int4)) ((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
((triple1 ((((((triple7) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow sees the lion.
("cow" "sees" "lion" "+")
int4
The cow does not see the cow.
False
5
inv-proof
[(((triple1 ((((triple4) -> rule5)) -> rule1)) -> rule3) OR ((triple3 ((triple5 ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((triple3 ((((triple7) -> rule7) ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((triple1 ((((((triple7) -> rule8)) -> rule5)) -> rule1)) -> rule3))]
("cow" "sees" "cow" "-")
((triple1 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
((triple3 ((triple5 ((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((triple3 ((((triple7) -> (rule7 % int4)) ((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
((triple1 ((((((triple7) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow sees the lion.
("cow" "sees" "lion" "+")
int4
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The cow does not need the lion.
Unknown
inv-random
[@0: The cow needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "lion" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The lion likes the cow.
Unknown
random
[@0: The lion likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cow" "+")
@0: The cow is cold.[(triple1)] The cow is young.[(triple2)] The cow likes the lion.[(triple3)] The cow sees the lion.[(triple4 OR ((triple7) -> rule8))] The lion is cold.[(triple5 OR ((triple7) -> rule7))] The lion is red.[(triple6)] The lion needs the cow.[(triple7)] @1: The cow is red.[(((triple4) -> rule5) OR ((((triple7) -> rule8)) -> rule5))] The lion is blue.[(((triple6) -> rule1))] @2: The cow is blue.[(((((triple4) -> rule5)) -> rule1) OR ((((((triple7) -> rule8)) -> rule5)) -> rule1))] The lion sees the cow.[(((triple5 ((triple6) -> rule1)) -> rule3) OR ((((triple7) -> rule7) ((triple6) -> rule1)) -> rule3))] @3: The cow sees the cow.[(((triple1 ((((triple4) -> rule5)) -> rule1)) -> rule3) OR ((triple3 ((triple5 ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((triple3 ((((triple7) -> rule7) ((triple6) -> rule1)) -> rule3)) -> rule2) OR ((triple1 ((((((triple7) -> rule8)) -> rule5)) -> rule1)) -> rule3))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow likes the lion.
("cow" "likes" "lion" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
((triple7) -> (rule8 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple5
((triple7) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
triple6
The lion needs the cow.
("lion" "needs" "cow" "+")
triple7
The cow is red.
("cow" "is" "red" "+")
((triple4) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((((triple7) -> (rule8 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
((triple6) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
((((((triple7) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow sees the lion.
("cow" "sees" "lion" "+")
int3
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple5 ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple7) -> (rule7 % int3)) ((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple1 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
((triple3 ((triple5 ((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((triple3 ((((triple7) -> (rule7 % int4)) ((triple6) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
((triple1 ((((((triple7) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow sees the lion.
("cow" "sees" "lion" "+")
int4