The bear eats the cat. The cat visits the bear. If someone eats the bear then they eat the cat. If someone sees the cat and they are big then they are round. If someone visits the cat and they see the cat then they are green. If someone visits the bear then the bear eats the cat. If someone sees the cat then they eat the bear. If someone visits the bear and the bear eats the cat then they see the cat. If someone sees the bear then the bear eats the cat. If someone eats the bear and the bear is cold then they are red.
The bear eats the cat.
("bear" "eats" "cat" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If someone eats the bear then they eat the cat.
((("someone" "eats" "bear" "+")) -> ("someone" "eats" "cat" "+"))
If someone sees the cat and they are big then they are round.
((("someone" "sees" "cat" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone visits the cat and they see the cat then they are green.
((("someone" "visits" "cat" "+") ("someone" "sees" "cat" "+")) -> ("someone" "is" "green" "+"))
If someone visits the bear then the bear eats the cat.
((("someone" "visits" "bear" "+")) -> ("bear" "eats" "cat" "+"))
If someone sees the cat then they eat the bear.
((("someone" "sees" "cat" "+")) -> ("someone" "eats" "bear" "+"))
If someone visits the bear and the bear eats the cat then they see the cat.
((("someone" "visits" "bear" "+") ("bear" "eats" "cat" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the bear then the bear eats the cat.
((("someone" "sees" "bear" "+")) -> ("bear" "eats" "cat" "+"))
If someone eats the bear and the bear is cold then they are red.
((("someone" "eats" "bear" "+") ("bear" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
The bear eats the cat.
True
1
proof
[(triple1 OR ((triple2) -> rule4))]
("bear" "eats" "cat" "+")
triple1
((triple2) -> (rule4 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat does not visit the bear.
False
1
inv-proof
[(triple2)]
("cat" "visits" "bear" "-")
triple2
The cat sees the cat.
True
3
proof
[(((triple2 triple1) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule6))]
("cat" "sees" "cat" "+")
((triple2 triple1) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The cat does not see the cat.
False
3
inv-proof
[(((triple2 triple1) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule6))]
("cat" "sees" "cat" "-")
((triple2 triple1) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The cat eats the bear.
True
4
proof
[(((((triple2 triple1) -> rule6)) -> rule5) OR ((((triple2 ((triple2) -> rule4)) -> rule6)) -> rule5))]
("cat" "eats" "bear" "+")
((((triple2 triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The bear eats the cat.
("bear" "eats" "cat" "+")
int3
The cat does not eat the bear.
False
4
inv-proof
[(((((triple2 triple1) -> rule6)) -> rule5) OR ((((triple2 ((triple2) -> rule4)) -> rule6)) -> rule5))]
("cat" "eats" "bear" "-")
((((triple2 triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The bear eats the cat.
("bear" "eats" "cat" "+")
int3
The bear is not green.
Unknown
inv-rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "green" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "round" "+")
The bear does not see the cat.
Unknown
inv-rconc
[@1: The bear sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "sees" "cat" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The bear eats the cat.[(triple1 OR ((triple2) -> rule4))] The cat visits the bear.[(triple2)] @1: The cat sees the cat.[(((triple2 triple1) -> rule6) OR ((triple2 ((triple2) -> rule4)) -> rule6))] @2: The cat eats the bear.[(((((triple2 triple1) -> rule6)) -> rule5) OR ((((triple2 ((triple2) -> rule4)) -> rule6)) -> rule5))] @3: The cat eats the cat.[(((((((triple2 triple1) -> rule6)) -> rule5)) -> rule1) OR ((((((triple2 ((triple2) -> rule4)) -> rule6)) -> rule5)) -> rule1))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
((triple2) -> (rule4 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
triple2
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple2 triple1) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
((triple2 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The bear eats the cat.
("bear" "eats" "cat" "+")
int2
The cat eats the bear.
("cat" "eats" "bear" "+")
((((triple2 triple1) -> (rule6 % int2))) -> (rule5 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The bear eats the cat.
("bear" "eats" "cat" "+")
int3
The cat eats the cat.
("cat" "eats" "cat" "+")
((((((triple2 triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
int3
((((((triple2 ((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
int3
The bear eats the cat.
("bear" "eats" "cat" "+")
int4