The cow is green. The cow is rough. The cow visits the mouse. The cow visits the tiger. The mouse chases the cow. The mouse is not young. The mouse sees the cow. The mouse sees the tiger. The tiger chases the mouse. The tiger is round. The tiger sees the mouse. The tiger visits the cow. If the tiger chases the mouse then the mouse is round. If something sees the cow and it sees the mouse then it does not chase the cow. If something visits the mouse then it sees the cow. If something is round then it sees the cow. If something visits the tiger and the tiger visits the mouse then the tiger visits the cow. If something is nice and not round then it does not visit the mouse.
The cow is green.
("cow" "is" "green" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If the tiger chases the mouse then the mouse is round.
((("tiger" "chases" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If something sees the cow and it sees the mouse then it does not chase the cow.
((("something" "sees" "cow" "+") ("something" "sees" "mouse" "+")) -> ("something" "chases" "cow" "-"))
If something visits the mouse then it sees the cow.
((("something" "visits" "mouse" "+")) -> ("something" "sees" "cow" "+"))
If something is round then it sees the cow.
((("something" "is" "round" "+")) -> ("something" "sees" "cow" "+"))
If something visits the tiger and the tiger visits the mouse then the tiger visits the cow.
((("something" "visits" "tiger" "+") ("tiger" "visits" "mouse" "+")) -> ("tiger" "visits" "cow" "+"))
If something is nice and not round then it does not visit the mouse.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "visits" "mouse" "-"))
The mouse sees the cow.
True
1
proof
[(triple7 OR ((((triple9) -> rule1)) -> rule4))]
("mouse" "sees" "cow" "+")
triple7
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse does not see the tiger.
False
1
inv-proof
[(triple8)]
("mouse" "sees" "tiger" "-")
triple8
The mouse is round.
True
2
proof
[(((triple9) -> rule1))]
("mouse" "is" "round" "+")
((triple9) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "sees" "cow" "-")
((triple3) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The tiger does not chase the cow.
True
4
proof
[(((((triple10) -> rule4) triple11) -> rule2))]
("tiger" "chases" "cow" "-")
((((triple10) -> (rule4 % int2)) triple11) -> (rule2 % int1))
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The tiger chases the cow.
False
4
inv-proof
[(((((triple10) -> rule4) triple11) -> rule2))]
("tiger" "chases" "cow" "+")
((((triple10) -> (rule4 % int2)) triple11) -> (rule2 % int1))
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The cow does not chase the mouse.
Unknown
inv-random
[@0: The cow chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "mouse" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The cow is green.[(triple1)] The cow is rough.[(triple2)] The cow visits the mouse.[(triple3)] The cow visits the tiger.[(triple4)] The mouse chases the cow.[(triple5)] The mouse is not young.[(triple6)] The mouse sees the cow.[(triple7 OR ((((triple9) -> rule1)) -> rule4))] The mouse sees the tiger.[(triple8)] The tiger chases the mouse.[(triple9)] The tiger is round.[(triple10)] The tiger sees the mouse.[(triple11)] The tiger visits the cow.[(triple12)] @1: The cow sees the cow.[(((triple3) -> rule3))] The mouse is round.[(((triple9) -> rule1))] The tiger sees the cow.[(((triple10) -> rule4))] @2: The tiger does not chase the cow.[(((((triple10) -> rule4) triple11) -> rule2))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple3
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple4
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple5
The mouse is not young.
("mouse" "is" "young" "-")
triple6
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple7
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple8
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple11
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple12
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple3) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple9) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
((triple10) -> (rule4 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
((((triple10) -> (rule4 % int2)) triple11) -> (rule2 % int1))
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int2