The cow eats the dog. The cow is cold. The cow is green. The cow is nice. The cow is round. The cow is young. The cow needs the dog. The cow visits the dog. The dog eats the cow. The dog is cold. The dog is green. The dog is round. The dog is young. The dog needs the cow. The dog visits the cow. If someone needs the dog then the dog is young. If someone eats the cow then they need the cow. If someone visits the cow then they eat the cow. If someone needs the cow then they visit the cow. If the dog eats the cow then the dog visits the cow. If someone eats the dog then they visit the cow.
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
If someone needs the dog then the dog is young.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "young" "+"))
If someone eats the cow then they need the cow.
((("someone" "eats" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If someone visits the cow then they eat the cow.
((("someone" "visits" "cow" "+")) -> ("someone" "eats" "cow" "+"))
If someone needs the cow then they visit the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If the dog eats the cow then the dog visits the cow.
((("dog" "eats" "cow" "+")) -> ("dog" "visits" "cow" "+"))
If someone eats the dog then they visit the cow.
((("someone" "eats" "dog" "+")) -> ("someone" "visits" "cow" "+"))
The cow eats the dog.
True
1
proof
[(triple1)]
("cow" "eats" "dog" "+")
triple1
The cow is not nice.
False
1
inv-proof
[(triple4)]
("cow" "is" "nice" "-")
triple4
The cow visits the cow.
True
2
proof
[(((triple1) -> rule6))]
("cow" "visits" "cow" "+")
((triple1) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple1) -> rule6))]
("cow" "visits" "cow" "-")
((triple1) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the cow.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("cow" "eats" "cow" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow does not eat the cow.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("cow" "eats" "cow" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "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 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 cold.[(triple2)] The cow is green.[(triple3)] The cow is nice.[(triple4)] The cow is round.[(triple5)] The cow is young.[(triple6)] The cow needs the dog.[(triple7)] The cow visits the dog.[(triple8)] The dog eats the cow.[(triple9 OR ((triple15) -> rule3) OR ((((triple14) -> rule4)) -> rule3))] The dog is cold.[(triple10)] The dog is green.[(triple11)] The dog is round.[(triple12)] The dog is young.[(triple13 OR ((triple7) -> rule1))] The dog needs the cow.[(triple14 OR ((triple9) -> rule2) OR ((((triple15) -> rule3)) -> rule2))] The dog visits the cow.[(triple15 OR ((triple14) -> rule4) OR ((triple9) -> rule5) OR ((((triple9) -> rule2)) -> rule4))] @1: The cow visits the cow.[(((triple1) -> rule6))] @2: The cow eats the cow.[(((((triple1) -> rule6)) -> rule3))] @3: The cow needs the cow.[(((((((triple1) -> rule6)) -> rule3)) -> rule2))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5
The cow is young.
("cow" "is" "young" "+")
triple6
The cow needs the dog.
("cow" "needs" "dog" "+")
triple7
The cow visits the dog.
("cow" "visits" "dog" "+")
triple8
The dog eats the cow.
("dog" "eats" "cow" "+")
triple9
((triple15) -> (rule3 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
((((triple14) -> (rule4 % int2))) -> (rule3 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
triple10
The dog is green.
("dog" "is" "green" "+")
triple11
The dog is round.
("dog" "is" "round" "+")
triple12
The dog is young.
("dog" "is" "young" "+")
triple13
((triple7) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
triple14
((triple9) -> (rule2 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
triple15
((triple14) -> (rule4 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
((triple9) -> (rule5 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1) -> (rule6 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3