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