The bear eats the cow. The cow is red. The dog is red. The mouse sees the cow. If something is red then it eats the cow.
The bear eats the cow.
("bear" "eats" "cow" "+")
The cow is red.
("cow" "is" "red" "+")
The dog is red.
("dog" "is" "red" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something is red then it eats the cow.
((("something" "is" "red" "+")) -> ("something" "eats" "cow" "+"))
The cow is red.
True
1
proof
[(triple2)]
("cow" "is" "red" "+")
triple2
The bear does not eat the cow.
False
1
inv-proof
[(triple1)]
("bear" "eats" "cow" "-")
triple1
The cow eats the cow.
True
2
proof
[(((triple2) -> rule1))]
("cow" "eats" "cow" "+")
((triple2) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The dog does not eat the cow.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "eats" "cow" "-")
((triple3) -> (rule1 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The mouse does not eat the cow.
Unknown
inv-rconc
[@1: The mouse eats the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "cow" "-")
The dog sees the cow.
Unknown
random
[@0: The dog sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cow" "+")
The bear does not chase the mouse.
Unknown
inv-random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "-")
The dog eats the mouse.
Unknown
random
[@0: The dog eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "mouse" "+")
@0: The bear eats the cow.[(triple1)] The cow is red.[(triple2)] The dog is red.[(triple3)] The mouse sees the cow.[(triple4)] @1: The cow eats the cow.[(((triple2) -> rule1))] The dog eats the cow.[(((triple3) -> rule1))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple4
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple2) -> (rule1 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
((triple3) -> (rule1 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1