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