The bear sees the squirrel. The cat chases the mouse. The mouse sees the bear. The squirrel is big. Round things are green. If something sees the squirrel and it visits the squirrel then it is round. If something sees the squirrel and it sees the cat then it visits the cat. If the squirrel chases the bear and the squirrel chases the mouse then the bear visits the cat. If something visits the mouse and the mouse is red then it is big. If something sees the bear then the bear visits the squirrel. If the mouse is big and the mouse visits the cat then the cat sees the mouse. If something is big and it chases the bear then it visits the squirrel.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something sees the squirrel and it visits the squirrel then it is round.
((("something" "sees" "squirrel" "+") ("something" "visits" "squirrel" "+")) -> ("something" "is" "round" "+"))
If something sees the squirrel and it sees the cat then it visits the cat.
((("something" "sees" "squirrel" "+") ("something" "sees" "cat" "+")) -> ("something" "visits" "cat" "+"))
If the squirrel chases the bear and the squirrel chases the mouse then the bear visits the cat.
((("squirrel" "chases" "bear" "+") ("squirrel" "chases" "mouse" "+")) -> ("bear" "visits" "cat" "+"))
If something visits the mouse and the mouse is red then it is big.
((("something" "visits" "mouse" "+") ("mouse" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something sees the bear then the bear visits the squirrel.
((("something" "sees" "bear" "+")) -> ("bear" "visits" "squirrel" "+"))
If the mouse is big and the mouse visits the cat then the cat sees the mouse.
((("mouse" "is" "big" "+") ("mouse" "visits" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If something is big and it chases the bear then it visits the squirrel.
((("something" "is" "big" "+") ("something" "chases" "bear" "+")) -> ("something" "visits" "squirrel" "+"))
The mouse sees the bear.
True
1
proof
[(triple3)]
("mouse" "sees" "bear" "+")
triple3
The mouse does not see the bear.
False
1
inv-proof
[(triple3)]
("mouse" "sees" "bear" "-")
triple3
The bear visits the squirrel.
True
2
proof
[(((triple3) -> rule6))]
("bear" "visits" "squirrel" "+")
((triple3) -> (rule6 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The bear does not visit the squirrel.
False
2
inv-proof
[(((triple3) -> rule6))]
("bear" "visits" "squirrel" "-")
((triple3) -> (rule6 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The bear is round.
True
4
proof
[(((triple1 ((triple3) -> rule6)) -> rule2))]
("bear" "is" "round" "+")
((triple1 ((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2
The bear is not round.
False
4
inv-proof
[(((triple1 ((triple3) -> rule6)) -> rule2))]
("bear" "is" "round" "-")
((triple1 ((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2
The bear is green.
True
5
proof
[(((((triple1 ((triple3) -> rule6)) -> rule2)) -> rule1))]
("bear" "is" "green" "+")
((((triple1 ((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int3
The bear is not green.
False
5
inv-proof
[(((((triple1 ((triple3) -> rule6)) -> rule2)) -> rule1))]
("bear" "is" "green" "-")
((((triple1 ((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int3
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "round" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The squirrel does not visit the cat.
Unknown
inv-rconc
[@1: The squirrel visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "cat" "-")
The squirrel is round.
Unknown
rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "round" "+")
The squirrel does not visit the bear.
Unknown
inv-random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "-")
The bear visits the mouse.
Unknown
random
[@0: The bear visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "mouse" "+")
The squirrel does not chase the cat.
Unknown
inv-random
[@0: The squirrel chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "cat" "-")
The squirrel visits the mouse.
Unknown
random
[@0: The squirrel visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "mouse" "+")
@0: The bear sees the squirrel.[(triple1)] The cat chases the mouse.[(triple2)] The mouse sees the bear.[(triple3)] The squirrel is big.[(triple4)] @1: The bear visits the squirrel.[(((triple3) -> rule6))] @2: The bear is round.[(((triple1 ((triple3) -> rule6)) -> rule2))] @3: The bear is green.[(((((triple1 ((triple3) -> rule6)) -> rule2)) -> rule1))]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple2
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple3
The squirrel is big.
("squirrel" "is" "big" "+")
triple4
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
((triple3) -> (rule6 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The bear is round.
("bear" "is" "round" "+")
((triple1 ((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2
The bear is green.
("bear" "is" "green" "+")
((((triple1 ((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int3