The cow chases the mouse. The cow eats the mouse. The cow is big. The cow is young. The cow visits the mouse. The mouse chases the cow. The mouse eats the cow. The mouse is green. The mouse is kind. The mouse is red. The mouse is young. The mouse visits the cow. If someone is big and kind then they eat the cow. If the cow chases the mouse then the mouse chases the cow. If someone visits the mouse then they are kind.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is young.
("cow" "is" "young" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If someone is big and kind then they eat the cow.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "eats" "cow" "+"))
If the cow chases the mouse then the mouse chases the cow.
((("cow" "chases" "mouse" "+")) -> ("mouse" "chases" "cow" "+"))
If someone visits the mouse then they are kind.
((("someone" "visits" "mouse" "+")) -> ("someone" "is" "kind" "+"))
The mouse chases the cow.
True
1
proof
[(triple6 OR ((triple1) -> rule2))]
("mouse" "chases" "cow" "+")
triple6
((triple1) -> (rule2 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The cow does not visit the mouse.
False
1
inv-proof
[(triple5)]
("cow" "visits" "mouse" "-")
triple5
The cow is kind.
True
2
proof
[(((triple5) -> rule3))]
("cow" "is" "kind" "+")
((triple5) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not kind.
False
2
inv-proof
[(((triple5) -> rule3))]
("cow" "is" "kind" "-")
((triple5) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow eats the cow.
True
4
proof
[(((triple3 ((triple5) -> rule3)) -> rule1))]
("cow" "eats" "cow" "+")
((triple3 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow does not eat the cow.
False
4
inv-proof
[(((triple3 ((triple5) -> rule3)) -> rule1))]
("cow" "eats" "cow" "-")
((triple3 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
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 visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The cow chases the mouse.[(triple1)] The cow eats the mouse.[(triple2)] The cow is big.[(triple3)] The cow is young.[(triple4)] The cow visits the mouse.[(triple5)] The mouse chases the cow.[(triple6 OR ((triple1) -> rule2))] The mouse eats the cow.[(triple7)] The mouse is green.[(triple8)] The mouse is kind.[(triple9)] The mouse is red.[(triple10)] The mouse is young.[(triple11)] The mouse visits the cow.[(triple12)] @1: The cow is kind.[(((triple5) -> rule3))] @2: The cow eats the cow.[(((triple3 ((triple5) -> rule3)) -> rule1))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple5
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple6
((triple1) -> (rule2 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse is kind.
("mouse" "is" "kind" "+")
triple9
The mouse is red.
("mouse" "is" "red" "+")
triple10
The mouse is young.
("mouse" "is" "young" "+")
triple11
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple12
The cow is kind.
("cow" "is" "kind" "+")
((triple5) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple3 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2