The cow eats the dog. The dog eats the rabbit. The dog is young. The rabbit eats the dog. The rabbit is rough. The rabbit needs the dog. The rabbit visits the dog. If something eats the dog then the dog is blue. If something needs the rabbit and it visits the rabbit then it needs the cow. If something visits the dog and it visits the rabbit then it is red. If something is rough then it visits the dog. If something needs the rabbit then it eats the cow. If something is rough then it needs the cow. If something eats the rabbit then it is rough. If something is red then it eats the dog.
The cow eats the dog.
("cow" "eats" "dog" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is young.
("dog" "is" "young" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If something eats the dog then the dog is blue.
((("something" "eats" "dog" "+")) -> ("dog" "is" "blue" "+"))
If something needs the rabbit and it visits the rabbit then it needs the cow.
((("something" "needs" "rabbit" "+") ("something" "visits" "rabbit" "+")) -> ("something" "needs" "cow" "+"))
If something visits the dog and it visits the rabbit then it is red.
((("something" "visits" "dog" "+") ("something" "visits" "rabbit" "+")) -> ("something" "is" "red" "+"))
If something is rough then it visits the dog.
((("something" "is" "rough" "+")) -> ("something" "visits" "dog" "+"))
If something needs the rabbit then it eats the cow.
((("something" "needs" "rabbit" "+")) -> ("something" "eats" "cow" "+"))
If something is rough then it needs the cow.
((("something" "is" "rough" "+")) -> ("something" "needs" "cow" "+"))
If something eats the rabbit then it is rough.
((("something" "eats" "rabbit" "+")) -> ("something" "is" "rough" "+"))
If something is red then it eats the dog.
((("something" "is" "red" "+")) -> ("something" "eats" "dog" "+"))
The dog eats the rabbit.
True
1
proof
[(triple2)]
("dog" "eats" "rabbit" "+")
triple2
The rabbit does not need the dog.
False
1
inv-proof
[(triple6)]
("rabbit" "needs" "dog" "-")
triple6
The dog is blue.
True
2
proof
[(((triple1) -> rule1) OR ((triple4) -> rule1))]
("dog" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple4) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not blue.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple4) -> rule1))]
("dog" "is" "blue" "-")
((triple1) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple4) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog visits the dog.
True
3
proof
[(((((triple2) -> rule7)) -> rule4))]
("dog" "visits" "dog" "+")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog does not need the cow.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule6))]
("dog" "needs" "cow" "-")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog does not eat the dog.
Unknown
inv-rconc
[@2: The dog eats the dog.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("dog" "eats" "dog" "-")
The cow visits the dog.
Unknown
rconc
[@2: The cow visits the dog.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("cow" "visits" "dog" "+")
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "rough" "-")
The dog visits the cow.
Unknown
random
[@0: The dog visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cow" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The cow needs the rabbit.
Unknown
random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "+")
@0: The cow eats the dog.[(triple1)] The dog eats the rabbit.[(triple2)] The dog is young.[(triple3)] The rabbit eats the dog.[(triple4)] The rabbit is rough.[(triple5)] The rabbit needs the dog.[(triple6)] The rabbit visits the dog.[(triple7 OR ((triple5) -> rule4))] @1: The dog is blue.[(((triple1) -> rule1) OR ((triple4) -> rule1))] The dog is rough.[(((triple2) -> rule7))] The rabbit needs the cow.[(((triple5) -> rule6))] @2: The dog needs the cow.[(((((triple2) -> rule7)) -> rule6))] The dog visits the dog.[(((((triple2) -> rule7)) -> rule4))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple6
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple7
((triple5) -> (rule4 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple4) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((triple2) -> (rule7 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((triple5) -> (rule6 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2