The cow eats the dog. The cow is blue. The cow is nice. The cow is young. The cow needs the dog. The cow sees the dog. The dog eats the cow. The dog is rough. The dog is round. The dog is young. The dog needs the cow. The dog sees the cow. If something needs the cow then it eats the cow. If something sees the cow then it is nice. If something eats the cow then the cow is round. If something is nice and it eats the dog then the dog sees the cow. If the cow needs the dog and the dog needs the cow then the dog is young. If something is round then it needs the cow.
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If something needs the cow then it eats the cow.
((("something" "needs" "cow" "+")) -> ("something" "eats" "cow" "+"))
If something sees the cow then it is nice.
((("something" "sees" "cow" "+")) -> ("something" "is" "nice" "+"))
If something eats the cow then the cow is round.
((("something" "eats" "cow" "+")) -> ("cow" "is" "round" "+"))
If something is nice and it eats the dog then the dog sees the cow.
((("something" "is" "nice" "+") ("something" "eats" "dog" "+")) -> ("dog" "sees" "cow" "+"))
If the cow needs the dog and the dog needs the cow then the dog is young.
((("cow" "needs" "dog" "+") ("dog" "needs" "cow" "+")) -> ("dog" "is" "young" "+"))
If something is round then it needs the cow.
((("something" "is" "round" "+")) -> ("something" "needs" "cow" "+"))
The cow is nice.
True
1
proof
[(triple3)]
("cow" "is" "nice" "+")
triple3
The dog is not young.
False
1
inv-proof
[(triple10 OR ((triple5 triple11) -> rule5) OR ((triple5 ((triple9) -> rule6)) -> rule5))]
("dog" "is" "young" "-")
triple10
((triple5 triple11) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((triple5 ((triple9) -> (rule6 % int2))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The cow is round.
True
2
proof
[(((triple7) -> rule3) OR ((((triple11) -> rule1)) -> rule3) OR ((((((triple9) -> rule6)) -> rule1)) -> rule3))]
("cow" "is" "round" "+")
((triple7) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
int3
The dog is not nice.
False
2
inv-proof
[(((triple12) -> rule2) OR ((((triple3 triple1) -> rule4)) -> rule2))]
("dog" "is" "nice" "-")
((triple12) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
((((triple3 triple1) -> (rule4 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow needs the cow.
True
3
proof
[(((((triple7) -> rule3)) -> rule6) OR ((((((triple11) -> rule1)) -> rule3)) -> rule6) OR ((((((((triple9) -> rule6)) -> rule1)) -> rule3)) -> rule6))]
("cow" "needs" "cow" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
((((((triple11) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3
((((((((triple9) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3
The dog needs the cow.
("dog" "needs" "cow" "+")
int4
The cow does not need the cow.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule6) OR ((((((triple11) -> rule1)) -> rule3)) -> rule6) OR ((((((((triple9) -> rule6)) -> rule1)) -> rule3)) -> rule6))]
("cow" "needs" "cow" "-")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
((((((triple11) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3
((((((((triple9) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3
The dog needs the cow.
("dog" "needs" "cow" "+")
int4
The cow eats the cow.
True
4
proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule1) OR ((((((((triple11) -> rule1)) -> rule3)) -> rule6)) -> rule1) OR ((((((((((triple9) -> rule6)) -> rule1)) -> rule3)) -> rule6)) -> rule1))]
("cow" "eats" "cow" "+")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
((((((((triple11) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The dog eats the cow.
("dog" "eats" "cow" "+")
int4
((((((((((triple9) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The dog eats the cow.
("dog" "eats" "cow" "+")
int4
The dog needs the cow.
("dog" "needs" "cow" "+")
int5
The cow does not eat the cow.
False
4
inv-proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule1) OR ((((((((triple11) -> rule1)) -> rule3)) -> rule6)) -> rule1) OR ((((((((((triple9) -> rule6)) -> rule1)) -> rule3)) -> rule6)) -> rule1))]
("cow" "eats" "cow" "-")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
((((((((triple11) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The dog eats the cow.
("dog" "eats" "cow" "+")
int4
((((((((((triple9) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The dog eats the cow.
("dog" "eats" "cow" "+")
int4
The dog needs the cow.
("dog" "needs" "cow" "+")
int5
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The cow eats the dog.[(triple1)] The cow is blue.[(triple2)] The cow is nice.[(triple3)] The cow is young.[(triple4)] The cow needs the dog.[(triple5)] The cow sees the dog.[(triple6)] The dog eats the cow.[(triple7 OR ((triple11) -> rule1) OR ((((triple9) -> rule6)) -> rule1))] The dog is rough.[(triple8)] The dog is round.[(triple9)] The dog is young.[(triple10 OR ((triple5 triple11) -> rule5) OR ((triple5 ((triple9) -> rule6)) -> rule5))] The dog needs the cow.[(triple11 OR ((triple9) -> rule6))] The dog sees the cow.[(triple12 OR ((triple3 triple1) -> rule4))] @1: The cow is round.[(((triple7) -> rule3) OR ((((triple11) -> rule1)) -> rule3) OR ((((((triple9) -> rule6)) -> rule1)) -> rule3))] The dog is nice.[(((triple12) -> rule2) OR ((((triple3 triple1) -> rule4)) -> rule2))] @2: The cow needs the cow.[(((((triple7) -> rule3)) -> rule6) OR ((((((triple11) -> rule1)) -> rule3)) -> rule6) OR ((((((((triple9) -> rule6)) -> rule1)) -> rule3)) -> rule6))] @3: The cow eats the cow.[(((((((triple7) -> rule3)) -> rule6)) -> rule1) OR ((((((((triple11) -> rule1)) -> rule3)) -> rule6)) -> rule1) OR ((((((((((triple9) -> rule6)) -> rule1)) -> rule3)) -> rule6)) -> rule1))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The cow needs the dog.
("cow" "needs" "dog" "+")
triple5
The cow sees the dog.
("cow" "sees" "dog" "+")
triple6
The dog eats the cow.
("dog" "eats" "cow" "+")
triple7
((triple11) -> (rule1 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule1 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
triple8
The dog is round.
("dog" "is" "round" "+")
triple9
The dog is young.
("dog" "is" "young" "+")
triple10
((triple5 triple11) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((triple5 ((triple9) -> (rule6 % int2))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
triple11
((triple9) -> (rule6 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
triple12
((triple3 triple1) -> (rule4 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((triple7) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
int3
The dog is nice.
("dog" "is" "nice" "+")
((triple12) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
((((triple3 triple1) -> (rule4 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
((((((triple11) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3
((((((((triple9) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The dog eats the cow.
("dog" "eats" "cow" "+")
int3
The dog needs the cow.
("dog" "needs" "cow" "+")
int4
The cow eats the cow.
("cow" "eats" "cow" "+")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
((((((((triple11) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The dog eats the cow.
("dog" "eats" "cow" "+")
int4
((((((((((triple9) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The dog eats the cow.
("dog" "eats" "cow" "+")
int4
The dog needs the cow.
("dog" "needs" "cow" "+")
int5