The cat is big. The cat is young. The cat needs the cow. The cat visits the cow. The cow is green. The cow is red. The cow is young. The cow needs the cat. The cow sees the cat. The cow visits the cat. If something sees the cow and the cow sees the cat then the cow visits the cat. If the cow needs the cat and the cow is red then the cat sees the cow. If something is red then it needs the cow. If something needs the cat then the cat visits the cow. If something sees the cow then the cow is nice. If something visits the cat and the cat visits the cow then it needs the cow.
The cat is big.
("cat" "is" "big" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If something sees the cow and the cow sees the cat then the cow visits the cat.
((("something" "sees" "cow" "+") ("cow" "sees" "cat" "+")) -> ("cow" "visits" "cat" "+"))
If the cow needs the cat and the cow is red then the cat sees the cow.
((("cow" "needs" "cat" "+") ("cow" "is" "red" "+")) -> ("cat" "sees" "cow" "+"))
If something is red then it needs the cow.
((("something" "is" "red" "+")) -> ("something" "needs" "cow" "+"))
If something needs the cat then the cat visits the cow.
((("something" "needs" "cat" "+")) -> ("cat" "visits" "cow" "+"))
If something sees the cow then the cow is nice.
((("something" "sees" "cow" "+")) -> ("cow" "is" "nice" "+"))
If something visits the cat and the cat visits the cow then it needs the cow.
((("something" "visits" "cat" "+") ("cat" "visits" "cow" "+")) -> ("something" "needs" "cow" "+"))
The cow is young.
True
1
proof
[(triple7)]
("cow" "is" "young" "+")
triple7
The cow is not young.
False
1
inv-proof
[(triple7)]
("cow" "is" "young" "-")
triple7
The cow needs the cow.
True
2
proof
[(((triple6) -> rule3) OR ((triple10 triple4) -> rule6) OR ((triple10 ((triple8) -> rule4)) -> rule6) OR ((((((triple8 triple6) -> rule2) triple9) -> rule1) triple4) -> rule6) OR ((((((triple8 triple6) -> rule2) triple9) -> rule1) ((triple8) -> rule4)) -> rule6))]
("cow" "needs" "cow" "+")
((triple6) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple10 triple4) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple10 ((triple8) -> (rule4 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
int2
((((((triple8 triple6) -> (rule2 % int3)) triple9) -> (rule1 % int2)) triple4) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
((((((triple8 triple6) -> (rule2 % int4)) triple9) -> (rule1 % int3)) ((triple8) -> (rule4 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
int3
The cat sees the cow.
("cat" "sees" "cow" "+")
int4
The cat does not see the cow.
False
3
inv-proof
[(((triple8 triple6) -> rule2))]
("cat" "sees" "cow" "-")
((triple8 triple6) -> (rule2 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cow is nice.
True
4
proof
[(((((triple8 triple6) -> rule2)) -> rule5))]
("cow" "is" "nice" "+")
((((triple8 triple6) -> (rule2 % int2))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cow is not nice.
False
4
inv-proof
[(((((triple8 triple6) -> rule2)) -> rule5))]
("cow" "is" "nice" "-")
((((triple8 triple6) -> (rule2 % int2))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
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 cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat is big.[(triple1)] The cat is young.[(triple2)] The cat needs the cow.[(triple3)] The cat visits the cow.[(triple4 OR ((triple8) -> rule4))] The cow is green.[(triple5)] The cow is red.[(triple6)] The cow is young.[(triple7)] The cow needs the cat.[(triple8)] The cow sees the cat.[(triple9)] The cow visits the cat.[(triple10 OR ((((triple8 triple6) -> rule2) triple9) -> rule1))] @1: The cat sees the cow.[(((triple8 triple6) -> rule2))] The cow needs the cow.[(((triple6) -> rule3) OR ((triple10 triple4) -> rule6) OR ((triple10 ((triple8) -> rule4)) -> rule6) OR ((((((triple8 triple6) -> rule2) triple9) -> rule1) triple4) -> rule6) OR ((((((triple8 triple6) -> rule2) triple9) -> rule1) ((triple8) -> rule4)) -> rule6))] @2: The cow is nice.[(((((triple8 triple6) -> rule2)) -> rule5))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat needs the cow.
("cat" "needs" "cow" "+")
triple3
The cat visits the cow.
("cat" "visits" "cow" "+")
triple4
((triple8) -> (rule4 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
triple5
The cow is red.
("cow" "is" "red" "+")
triple6
The cow is young.
("cow" "is" "young" "+")
triple7
The cow needs the cat.
("cow" "needs" "cat" "+")
triple8
The cow sees the cat.
("cow" "sees" "cat" "+")
triple9
The cow visits the cat.
("cow" "visits" "cat" "+")
triple10
((((triple8 triple6) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
((triple8 triple6) -> (rule2 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple6) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple10 triple4) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple10 ((triple8) -> (rule4 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
int2
((((((triple8 triple6) -> (rule2 % int3)) triple9) -> (rule1 % int2)) triple4) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat sees the cow.
("cat" "sees" "cow" "+")
int3
((((((triple8 triple6) -> (rule2 % int4)) triple9) -> (rule1 % int3)) ((triple8) -> (rule4 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
int3
The cat sees the cow.
("cat" "sees" "cow" "+")
int4
The cow is nice.
("cow" "is" "nice" "+")
((((triple8 triple6) -> (rule2 % int2))) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2