The bear chases the cat. The bear is cold. The bear is green. The bear is round. The bear is young. The bear needs the cat. The bear visits the cat. The cat chases the bear. The cat is green. The cat is young. The cat needs the bear. The cat visits the bear. If the cat visits the bear and the bear does not visit the cat then the cat is red. If someone chases the cat and they do not visit the bear then the cat is red. If someone visits the bear and the bear is not round then they chase the cat. If someone is young then they chase the cat. If someone chases the cat then they chase the bear. If someone chases the cat then they are cold. Round people are green. If the cat visits the bear then the cat needs the bear.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If the cat visits the bear and the bear does not visit the cat then the cat is red.
((("cat" "visits" "bear" "+") ("bear" "visits" "cat" "~")) -> ("cat" "is" "red" "+"))
If someone chases the cat and they do not visit the bear then the cat is red.
((("someone" "chases" "cat" "+") ("someone" "visits" "bear" "~")) -> ("cat" "is" "red" "+"))
If someone visits the bear and the bear is not round then they chase the cat.
((("someone" "visits" "bear" "+") ("bear" "is" "round" "~")) -> ("someone" "chases" "cat" "+"))
If someone is young then they chase the cat.
((("someone" "is" "young" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cat then they chase the bear.
((("someone" "chases" "cat" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the cat then they are cold.
((("someone" "chases" "cat" "+")) -> ("someone" "is" "cold" "+"))
Round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If the cat visits the bear then the cat needs the bear.
((("cat" "visits" "bear" "+")) -> ("cat" "needs" "bear" "+"))
The bear chases the cat.
True
1
proof
[(triple1 OR ((triple5) -> rule4))]
("bear" "chases" "cat" "+")
triple1
((triple5) -> (rule4 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The cat is not green.
False
1
inv-proof
[(triple9)]
("cat" "is" "green" "-")
triple9
The cat chases the cat.
True
2
proof
[(((triple10) -> rule4))]
("cat" "chases" "cat" "+")
((triple10) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat does not chase the cat.
False
2
inv-proof
[(((triple10) -> rule4))]
("cat" "chases" "cat" "-")
((triple10) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is cold.
True
3
proof
[(((((triple10) -> rule4)) -> rule6))]
("cat" "is" "cold" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is not cold.
False
3
inv-proof
[(((((triple10) -> rule4)) -> rule6))]
("cat" "is" "cold" "-")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "red" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
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 needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The bear chases the cat.[(triple1 OR ((triple5) -> rule4))] The bear is cold.[(triple2 OR ((triple1) -> rule6) OR ((((triple5) -> rule4)) -> rule6))] The bear is green.[(triple3 OR ((triple4) -> rule7))] The bear is round.[(triple4)] The bear is young.[(triple5)] The bear needs the cat.[(triple6)] The bear visits the cat.[(triple7)] The cat chases the bear.[(triple8 OR ((((triple10) -> rule4)) -> rule5))] The cat is green.[(triple9)] The cat is young.[(triple10)] The cat needs the bear.[(triple11 OR ((triple12) -> rule8))] The cat visits the bear.[(triple12)] @1: The bear chases the bear.[(((triple1) -> rule5) OR ((((triple5) -> rule4)) -> rule5))] The cat chases the cat.[(((triple10) -> rule4))] @2: The cat is cold.[(((((triple10) -> rule4)) -> rule6))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
((triple5) -> (rule4 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
triple2
((triple1) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The bear is green.
("bear" "is" "green" "+")
triple3
((triple4) -> (rule7 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is round.
("bear" "is" "round" "+")
triple4
The bear is young.
("bear" "is" "young" "+")
triple5
The bear needs the cat.
("bear" "needs" "cat" "+")
triple6
The bear visits the cat.
("bear" "visits" "cat" "+")
triple7
The cat chases the bear.
("cat" "chases" "bear" "+")
triple8
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat is green.
("cat" "is" "green" "+")
triple9
The cat is young.
("cat" "is" "young" "+")
triple10
The cat needs the bear.
("cat" "needs" "bear" "+")
triple11
((triple12) -> (rule8 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
triple12
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple1) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple10) -> (rule4 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2