The cow eats the mouse. The cow is not blue. The cow visits the mouse. The dog eats the cow. The dog is kind. The mouse eats the squirrel. The mouse is kind. The squirrel eats the cow. The squirrel is round. The squirrel visits the cow. If someone is young and not big then they do not visit the squirrel. If someone visits the mouse and they are not blue then the mouse visits the cow. If someone visits the cow and the cow chases the mouse then they chase the cow. If someone chases the mouse then the mouse eats the cow. If someone eats the cow then the cow visits the dog. If someone eats the cow then they chase the mouse. If the cow eats the mouse and the cow is not young then the mouse is round. If someone chases the cow and they do not chase the mouse then the mouse is kind.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is kind.
("dog" "is" "kind" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If someone is young and not big then they do not visit the squirrel.
((("someone" "is" "young" "+") ("someone" "is" "big" "~")) -> ("someone" "visits" "squirrel" "-"))
If someone visits the mouse and they are not blue then the mouse visits the cow.
((("someone" "visits" "mouse" "+") ("someone" "is" "blue" "~")) -> ("mouse" "visits" "cow" "+"))
If someone visits the cow and the cow chases the mouse then they chase the cow.
((("someone" "visits" "cow" "+") ("cow" "chases" "mouse" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the mouse then the mouse eats the cow.
((("someone" "chases" "mouse" "+")) -> ("mouse" "eats" "cow" "+"))
If someone eats the cow then the cow visits the dog.
((("someone" "eats" "cow" "+")) -> ("cow" "visits" "dog" "+"))
If someone eats the cow then they chase the mouse.
((("someone" "eats" "cow" "+")) -> ("someone" "chases" "mouse" "+"))
If the cow eats the mouse and the cow is not young then the mouse is round.
((("cow" "eats" "mouse" "+") ("cow" "is" "young" "~")) -> ("mouse" "is" "round" "+"))
If someone chases the cow and they do not chase the mouse then the mouse is kind.
((("someone" "chases" "cow" "+") ("someone" "chases" "mouse" "~")) -> ("mouse" "is" "kind" "+"))
The mouse eats the squirrel.
True
1
proof
[(triple6)]
("mouse" "eats" "squirrel" "+")
triple6
The squirrel does not visit the cow.
False
1
inv-proof
[(triple10)]
("squirrel" "visits" "cow" "-")
triple10
The squirrel chases the mouse.
True
2
proof
[(((triple8) -> rule6))]
("squirrel" "chases" "mouse" "+")
((triple8) -> (rule6 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse does not visit the cow.
False
3
inv-proof
[(((triple3 triple2) -> rule2))]
("mouse" "visits" "cow" "-")
((triple3 triple2) -> (rule2 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse eats the cow.
True
3
proof
[(((((triple4) -> rule6)) -> rule4) OR ((((triple8) -> rule6)) -> rule4))]
("mouse" "eats" "cow" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse does not eat the cow.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule4) OR ((((triple8) -> rule6)) -> rule4))]
("mouse" "eats" "cow" "-")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse chases the mouse.
True
4
proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule6) OR ((((((triple8) -> rule6)) -> rule4)) -> rule6))]
("mouse" "chases" "mouse" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
((((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The mouse does not chase the mouse.
False
4
inv-proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule6) OR ((((((triple8) -> rule6)) -> rule4)) -> rule6))]
("mouse" "chases" "mouse" "-")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
((((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "chases" "cow" "-")
The squirrel chases the cow.
Unknown
rconc
[@2: The squirrel chases the cow.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("squirrel" "chases" "cow" "+")
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "round" "-")
The mouse chases the cow.
Unknown
rconc
[@2: The mouse chases the cow.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("mouse" "chases" "cow" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The cow eats the mouse.[(triple1)] The cow is not blue.[(triple2)] The cow visits the mouse.[(triple3)] The dog eats the cow.[(triple4)] The dog is kind.[(triple5)] The mouse eats the squirrel.[(triple6)] The mouse is kind.[(triple7)] The squirrel eats the cow.[(triple8)] The squirrel is round.[(triple9)] The squirrel visits the cow.[(triple10)] @1: The cow visits the dog.[(((triple4) -> rule5) OR ((triple8) -> rule5) OR ((((((triple4) -> rule6)) -> rule4)) -> rule5) OR ((((((triple8) -> rule6)) -> rule4)) -> rule5))] The dog chases the mouse.[(((triple4) -> rule6))] The mouse visits the cow.[(((triple3 triple2) -> rule2))] The squirrel chases the mouse.[(((triple8) -> rule6))] @2: The mouse eats the cow.[(((((triple4) -> rule6)) -> rule4) OR ((((triple8) -> rule6)) -> rule4))] @3: The mouse chases the mouse.[(((((((triple4) -> rule6)) -> rule4)) -> rule6) OR ((((((triple8) -> rule6)) -> rule4)) -> rule6))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow is not blue.
("cow" "is" "blue" "-")
triple2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple3
The dog eats the cow.
("dog" "eats" "cow" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple6
The mouse is kind.
("mouse" "is" "kind" "+")
triple7
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple10
The cow visits the dog.
("cow" "visits" "dog" "+")
((triple4) -> (rule5 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
((triple8) -> (rule5 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
((((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple4) -> (rule6 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((triple3 triple2) -> (rule2 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
((triple8) -> (rule6 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
((((triple8) -> (rule6 % int2))) -> (rule4 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
((((((triple8) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3