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