The bear chases the cat. The bear is big. The bear is not green. The bear is rough. The bear does not visit the cat. The cat chases the bear. The cat is kind. The cat is rough. The cat needs the bear. The cat visits the bear. If something is big then it chases the bear. Green things are not kind. If something is big and not red then it is kind. All green things are rough. If something visits the cat then it is rough. If the bear needs the cat and the cat does not need the bear then the cat does not visit the bear. If the bear visits the cat and the cat is big then the bear is green. If something chases the bear then it needs the cat.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is not green.
("bear" "is" "green" "-")
The bear is rough.
("bear" "is" "rough" "+")
The bear does not visit the cat.
("bear" "visits" "cat" "-")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If something is big then it chases the bear.
((("something" "is" "big" "+")) -> ("something" "chases" "bear" "+"))
Green things are not kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "-"))
If something is big and not red then it is kind.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "kind" "+"))
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something visits the cat then it is rough.
((("something" "visits" "cat" "+")) -> ("something" "is" "rough" "+"))
If the bear needs the cat and the cat does not need the bear then the cat does not visit the bear.
((("bear" "needs" "cat" "+") ("cat" "needs" "bear" "~")) -> ("cat" "visits" "bear" "-"))
If the bear visits the cat and the cat is big then the bear is green.
((("bear" "visits" "cat" "+") ("cat" "is" "big" "+")) -> ("bear" "is" "green" "+"))
If something chases the bear then it needs the cat.
((("something" "chases" "bear" "+")) -> ("something" "needs" "cat" "+"))
The bear chases the cat.
True
1
proof
[(triple1)]
("bear" "chases" "cat" "+")
triple1
The cat is not kind.
False
1
inv-proof
[(triple7)]
("cat" "is" "kind" "-")
triple7
The cat needs the cat.
True
2
proof
[(((triple6) -> rule8))]
("cat" "needs" "cat" "+")
((triple6) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The bear does not chase the bear.
False
2
inv-proof
[(((triple2) -> rule1))]
("bear" "chases" "bear" "-")
((triple2) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear needs the cat.
True
3
proof
[(((((triple2) -> rule1)) -> rule8))]
("bear" "needs" "cat" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear does not need the cat.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule8))]
("bear" "needs" "cat" "-")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "kind" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The bear chases the cat.[(triple1)] The bear does not visit the cat.[(triple5)] The bear is big.[(triple2)] The bear is not green.[(triple3)] The bear is rough.[(triple4)] The cat chases the bear.[(triple6)] The cat is kind.[(triple7)] The cat is rough.[(triple8)] The cat needs the bear.[(triple9)] The cat visits the bear.[(triple10)] @1: The bear chases the bear.[(((triple2) -> rule1))] The cat needs the cat.[(((triple6) -> rule8))] @2: The bear needs the cat.[(((((triple2) -> rule1)) -> rule8))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear does not visit the cat.
("bear" "visits" "cat" "-")
triple5
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is not green.
("bear" "is" "green" "-")
triple3
The bear is rough.
("bear" "is" "rough" "+")
triple4
The cat chases the bear.
("cat" "chases" "bear" "+")
triple6
The cat is kind.
("cat" "is" "kind" "+")
triple7
The cat is rough.
("cat" "is" "rough" "+")
triple8
The cat needs the bear.
("cat" "needs" "bear" "+")
triple9
The cat visits the bear.
("cat" "visits" "bear" "+")
triple10
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple2) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple6) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The bear needs the cat.
("bear" "needs" "cat" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2