The dog chases the squirrel. The mouse is big. The squirrel is rough. If something eats the mouse and it sees the dog then it chases the squirrel. If something sees the mouse and it does not eat the dog then it does not eat the squirrel. If something eats the mouse and it chases the mouse then the mouse is not rough. If something chases the dog then it sees the dog. If something chases the squirrel then it chases the dog. If something sees the mouse then it is rough.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The mouse is big.
("mouse" "is" "big" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If something eats the mouse and it sees the dog then it chases the squirrel.
((("something" "eats" "mouse" "+") ("something" "sees" "dog" "+")) -> ("something" "chases" "squirrel" "+"))
If something sees the mouse and it does not eat the dog then it does not eat the squirrel.
((("something" "sees" "mouse" "+") ("something" "eats" "dog" "~")) -> ("something" "eats" "squirrel" "-"))
If something eats the mouse and it chases the mouse then the mouse is not rough.
((("something" "eats" "mouse" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "is" "rough" "-"))
If something chases the dog then it sees the dog.
((("something" "chases" "dog" "+")) -> ("something" "sees" "dog" "+"))
If something chases the squirrel then it chases the dog.
((("something" "chases" "squirrel" "+")) -> ("something" "chases" "dog" "+"))
If something sees the mouse then it is rough.
((("something" "sees" "mouse" "+")) -> ("something" "is" "rough" "+"))
The mouse is big.
True
1
proof
[(triple2)]
("mouse" "is" "big" "+")
triple2
The mouse is not big.
False
1
inv-proof
[(triple2)]
("mouse" "is" "big" "-")
triple2
The dog chases the dog.
True
2
proof
[(((triple1) -> rule5))]
("dog" "chases" "dog" "+")
((triple1) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not chase the dog.
False
2
inv-proof
[(((triple1) -> rule5))]
("dog" "chases" "dog" "-")
((triple1) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog sees the dog.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("dog" "sees" "dog" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog does not see the dog.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("dog" "sees" "dog" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "rough" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The mouse does not chase the dog.
Unknown
inv-rconc
[@2: The mouse chases the dog.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("mouse" "chases" "dog" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
The mouse does not see the squirrel.
Unknown
inv-random
[@0: The mouse sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "squirrel" "-")
The mouse eats the dog.
Unknown
random
[@0: The mouse eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "dog" "+")
@0: The dog chases the squirrel.[(triple1)] The mouse is big.[(triple2)] The squirrel is rough.[(triple3)] @1: The dog chases the dog.[(((triple1) -> rule5))] @2: The dog sees the dog.[(((((triple1) -> rule5)) -> rule4))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple1) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2