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