The bear chases the rabbit. The bear eats the rabbit. The bear is blue. The bear sees the rabbit. The rabbit chases the bear. The rabbit eats the bear. The rabbit sees the bear. Round things are green. If something eats the bear then the bear is round. If something is rough then it sees the bear.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something eats the bear then the bear is round.
((("something" "eats" "bear" "+")) -> ("bear" "is" "round" "+"))
If something is rough then it sees the bear.
((("something" "is" "rough" "+")) -> ("something" "sees" "bear" "+"))
The rabbit eats the bear.
True
1
proof
[(triple6)]
("rabbit" "eats" "bear" "+")
triple6
The bear does not see the rabbit.
False
1
inv-proof
[(triple4)]
("bear" "sees" "rabbit" "-")
triple4
The bear is round.
True
2
proof
[(((triple6) -> rule2))]
("bear" "is" "round" "+")
((triple6) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is not round.
False
2
inv-proof
[(((triple6) -> rule2))]
("bear" "is" "round" "-")
((triple6) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is green.
True
3
proof
[(((((triple6) -> rule2)) -> rule1))]
("bear" "is" "green" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is not green.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("bear" "is" "green" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "green" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "bear" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear chases the rabbit.[(triple1)] The bear eats the rabbit.[(triple2)] The bear is blue.[(triple3)] The bear sees the rabbit.[(triple4)] The rabbit chases the bear.[(triple5)] The rabbit eats the bear.[(triple6)] The rabbit sees the bear.[(triple7)] @1: The bear is round.[(((triple6) -> rule2))] @2: The bear is green.[(((((triple6) -> rule2)) -> rule1))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple4
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple5
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple6
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple7
The bear is round.
("bear" "is" "round" "+")
((triple6) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is green.
("bear" "is" "green" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2