The cow eats the dog. The cow is green. The cow is red. The cow needs the dog. The cow sees the dog. The dog is blue. The dog sees the cow. If something sees the dog then it needs the cow. If something eats the cow then the cow sees the dog. All green things are young. If something is green and it sees the dog then the dog is green. If something eats the dog then the dog needs the cow. If something is red then it needs the cow.
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is red.
("cow" "is" "red" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If something sees the dog then it needs the cow.
((("something" "sees" "dog" "+")) -> ("something" "needs" "cow" "+"))
If something eats the cow then the cow sees the dog.
((("something" "eats" "cow" "+")) -> ("cow" "sees" "dog" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is green and it sees the dog then the dog is green.
((("something" "is" "green" "+") ("something" "sees" "dog" "+")) -> ("dog" "is" "green" "+"))
If something eats the dog then the dog needs the cow.
((("something" "eats" "dog" "+")) -> ("dog" "needs" "cow" "+"))
If something is red then it needs the cow.
((("something" "is" "red" "+")) -> ("something" "needs" "cow" "+"))
The cow needs the dog.
True
1
proof
[(triple4)]
("cow" "needs" "dog" "+")
triple4
The cow does not see the dog.
False
1
inv-proof
[(triple5)]
("cow" "sees" "dog" "-")
triple5
The cow needs the cow.
True
2
proof
[(((triple3) -> rule6) OR ((triple5) -> rule1))]
("cow" "needs" "cow" "+")
((triple3) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple5) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple3) -> rule6) OR ((triple5) -> rule1))]
("cow" "needs" "cow" "-")
((triple3) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple5) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The dog eats the cow.
Unknown
random
[@0: The dog eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cow" "+")
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 dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The cow eats the dog.[(triple1)] The cow is green.[(triple2)] The cow is red.[(triple3)] The cow needs the dog.[(triple4)] The cow sees the dog.[(triple5)] The dog is blue.[(triple6)] The dog sees the cow.[(triple7)] @1: The cow is young.[(((triple2) -> rule3))] The cow needs the cow.[(((triple3) -> rule6) OR ((triple5) -> rule1))] The dog is green.[(((triple2 triple5) -> rule4))] The dog needs the cow.[(((triple1) -> rule5))] @2: The dog is young.[(((((triple2 triple5) -> rule4)) -> rule3))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow needs the dog.
("cow" "needs" "dog" "+")
triple4
The cow sees the dog.
("cow" "sees" "dog" "+")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple6
The dog sees the cow.
("dog" "sees" "cow" "+")
triple7
The cow is young.
("cow" "is" "young" "+")
((triple2) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple3) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((triple5) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The dog is green.
("dog" "is" "green" "+")
((triple2 triple5) -> (rule4 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
((triple1) -> (rule5 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple2 triple5) -> (rule4 % int2))) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2