The bear sees the cat. The cat sees the bear. If something is rough then it chases the cat. If the cat sees the bear and the cat eats the bear then the cat is kind. If something is young and it sees the cat then it sees the bear. If something chases the cat and it sees the cat then it is rough. If the cat sees the bear then the bear is rough. If something sees the cat and the cat sees the bear then it eats the bear. If something chases the cat then it eats the bear. If something eats the cat and it is cold then it sees the bear.
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
If something is rough then it chases the cat.
((("something" "is" "rough" "+")) -> ("something" "chases" "cat" "+"))
If the cat sees the bear and the cat eats the bear then the cat is kind.
((("cat" "sees" "bear" "+") ("cat" "eats" "bear" "+")) -> ("cat" "is" "kind" "+"))
If something is young and it sees the cat then it sees the bear.
((("something" "is" "young" "+") ("something" "sees" "cat" "+")) -> ("something" "sees" "bear" "+"))
If something chases the cat and it sees the cat then it is rough.
((("something" "chases" "cat" "+") ("something" "sees" "cat" "+")) -> ("something" "is" "rough" "+"))
If the cat sees the bear then the bear is rough.
((("cat" "sees" "bear" "+")) -> ("bear" "is" "rough" "+"))
If something sees the cat and the cat sees the bear then it eats the bear.
((("something" "sees" "cat" "+") ("cat" "sees" "bear" "+")) -> ("something" "eats" "bear" "+"))
If something chases the cat then it eats the bear.
((("something" "chases" "cat" "+")) -> ("something" "eats" "bear" "+"))
If something eats the cat and it is cold then it sees the bear.
((("something" "eats" "cat" "+") ("something" "is" "cold" "+")) -> ("something" "sees" "bear" "+"))
The bear sees the cat.
True
1
proof
[(triple1)]
("bear" "sees" "cat" "+")
triple1
The cat does not see the bear.
False
1
inv-proof
[(triple2)]
("cat" "sees" "bear" "-")
triple2
The bear eats the bear.
True
3
proof
[(((triple1 triple2) -> rule6) OR ((((((triple2) -> rule5)) -> rule1)) -> rule7))]
("bear" "eats" "bear" "+")
((triple1 triple2) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The bear is not rough.
False
2
inv-proof
[(((triple2) -> rule5))]
("bear" "is" "rough" "-")
((triple2) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "rough" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "bear" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The bear sees the cat.[(triple1)] The cat sees the bear.[(triple2)] @1: The bear eats the bear.[(((triple1 triple2) -> rule6) OR ((((((triple2) -> rule5)) -> rule1)) -> rule7))] The bear is rough.[(((triple2) -> rule5))] @2: The bear chases the cat.[(((((triple2) -> rule5)) -> rule1))]
The bear sees the cat.
("bear" "sees" "cat" "+")
triple1
The cat sees the bear.
("cat" "sees" "bear" "+")
triple2
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple1 triple2) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The bear is rough.
("bear" "is" "rough" "+")
((triple2) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2