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