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