The bear eats the cow. The cat is blue. The cow visits the mouse. The mouse is rough. If something sees the cat and the cat sees the mouse then the cat is cold. If the mouse sees the cow then the mouse is rough. If something is blue then it sees the mouse. If something visits the cow then it visits the mouse. If something sees the mouse then it eats the mouse. If something is cold and it eats the cow then it eats the mouse. If something visits the cat then it eats the cow. If something visits the cat and the cat eats the bear then the cat is blue.
The bear eats the cow.
("bear" "eats" "cow" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
If something sees the cat and the cat sees the mouse then the cat is cold.
((("something" "sees" "cat" "+") ("cat" "sees" "mouse" "+")) -> ("cat" "is" "cold" "+"))
If the mouse sees the cow then the mouse is rough.
((("mouse" "sees" "cow" "+")) -> ("mouse" "is" "rough" "+"))
If something is blue then it sees the mouse.
((("something" "is" "blue" "+")) -> ("something" "sees" "mouse" "+"))
If something visits the cow then it visits the mouse.
((("something" "visits" "cow" "+")) -> ("something" "visits" "mouse" "+"))
If something sees the mouse then it eats the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
If something is cold and it eats the cow then it eats the mouse.
((("something" "is" "cold" "+") ("something" "eats" "cow" "+")) -> ("something" "eats" "mouse" "+"))
If something visits the cat then it eats the cow.
((("something" "visits" "cat" "+")) -> ("something" "eats" "cow" "+"))
If something visits the cat and the cat eats the bear then the cat is blue.
((("something" "visits" "cat" "+") ("cat" "eats" "bear" "+")) -> ("cat" "is" "blue" "+"))
The bear eats the cow.
True
1
proof
[(triple1)]
("bear" "eats" "cow" "+")
triple1
The bear does not eat the cow.
False
1
inv-proof
[(triple1)]
("bear" "eats" "cow" "-")
triple1
The cat sees the mouse.
True
2
proof
[(((triple2) -> rule3))]
("cat" "sees" "mouse" "+")
((triple2) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat does not see the mouse.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "sees" "mouse" "-")
((triple2) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat eats the mouse.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("cat" "eats" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat does not eat the mouse.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("cat" "eats" "mouse" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The mouse does not eat the cow.
Unknown
inv-rconc
[@1: The mouse eats the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "eats" "cow" "-")
The cat visits the mouse.
Unknown
rconc
[@1: The cat visits the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "mouse" "+")
The mouse does not eat the mouse.
Unknown
inv-rconc
[@2: The mouse eats the mouse.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The bear visits the cat.
Unknown
random
[@0: The bear visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cat" "+")
The bear does not eat the cat.
Unknown
inv-random
[@0: The bear eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cat" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The bear eats the cow.[(triple1)] The cat is blue.[(triple2)] The cow visits the mouse.[(triple3)] The mouse is rough.[(triple4)] @1: The cat sees the mouse.[(((triple2) -> rule3))] @2: The cat eats the mouse.[(((((triple2) -> rule3)) -> rule5))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((triple2) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2