The bear chases the lion. The bear is red. The cat chases the lion. The cat is green. The cat is round. The cat needs the bear. The cat visits the bear. The cat visits the lion. The lion needs the bear. The lion needs the cat. If someone needs the lion then the lion visits the cat. If someone chases the lion then the lion is round. If someone is kind and green then they are young. If someone needs the cat then they visit the lion. If the bear is red then the bear needs the lion. If someone visits the cat then the cat needs the bear. If someone chases the cat then the cat needs the lion. If someone is kind then they need the lion.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is red.
("bear" "is" "red" "+")
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If someone needs the lion then the lion visits the cat.
((("someone" "needs" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If someone chases the lion then the lion is round.
((("someone" "chases" "lion" "+")) -> ("lion" "is" "round" "+"))
If someone is kind and green then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone needs the cat then they visit the lion.
((("someone" "needs" "cat" "+")) -> ("someone" "visits" "lion" "+"))
If the bear is red then the bear needs the lion.
((("bear" "is" "red" "+")) -> ("bear" "needs" "lion" "+"))
If someone visits the cat then the cat needs the bear.
((("someone" "visits" "cat" "+")) -> ("cat" "needs" "bear" "+"))
If someone chases the cat then the cat needs the lion.
((("someone" "chases" "cat" "+")) -> ("cat" "needs" "lion" "+"))
If someone is kind then they need the lion.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "lion" "+"))
The cat visits the lion.
True
1
proof
[(triple8)]
("cat" "visits" "lion" "+")
triple8
The lion does not need the bear.
False
1
inv-proof
[(triple9)]
("lion" "needs" "bear" "-")
triple9
The lion visits the lion.
True
2
proof
[(((triple10) -> rule4))]
("lion" "visits" "lion" "+")
((triple10) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple10) -> rule4))]
("lion" "visits" "lion" "-")
((triple10) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the cat.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("lion" "visits" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The lion does not visit the cat.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("lion" "visits" "cat" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The cat does not need the lion.
Unknown
inv-rconc
[@1: The cat needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "needs" "lion" "-")
The bear visits the lion.
Unknown
rconc
[@1: The bear visits the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "lion" "+")
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "young" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The lion visits the bear.
Unknown
random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "+")
@0: The bear chases the lion.[(triple1)] The bear is red.[(triple2)] The cat chases the lion.[(triple3)] The cat is green.[(triple4)] The cat is round.[(triple5)] The cat needs the bear.[(triple6 OR ((((((triple2) -> rule5)) -> rule1)) -> rule6))] The cat visits the bear.[(triple7)] The cat visits the lion.[(triple8)] The lion needs the bear.[(triple9)] The lion needs the cat.[(triple10)] @1: The bear needs the lion.[(((triple2) -> rule5))] The lion is round.[(((triple1) -> rule2) OR ((triple3) -> rule2))] The lion visits the lion.[(((triple10) -> rule4))] @2: The lion visits the cat.[(((((triple2) -> rule5)) -> rule1))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The cat chases the lion.
("cat" "chases" "lion" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The cat needs the bear.
("cat" "needs" "bear" "+")
triple6
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The bear needs the lion.
("bear" "needs" "lion" "+")
int3
The cat visits the bear.
("cat" "visits" "bear" "+")
triple7
The cat visits the lion.
("cat" "visits" "lion" "+")
triple8
The lion needs the bear.
("lion" "needs" "bear" "+")
triple9
The lion needs the cat.
("lion" "needs" "cat" "+")
triple10
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple2) -> (rule5 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((triple1) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((triple3) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple10) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2