The bear chases the cat. The cat chases the cow. The cat is nice. The cat sees the bear. The cat visits the bear. The cow is blue. The lion sees the cat. If something chases the cow and it is big then it sees the cat. If something chases the cat and it sees the lion then it visits the lion. If the cat chases the lion then the cat sees the lion. If something sees the cow and the cow sees the cat then it visits the cat. If something visits the bear then it chases the lion. If something is red then it sees the lion. If something visits the cat and it visits the bear then the bear is red. If something is big and it visits the lion then it sees the bear.
The bear chases the cat.
("bear" "chases" "cat" "+")
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cow is blue.
("cow" "is" "blue" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If something chases the cow and it is big then it sees the cat.
((("something" "chases" "cow" "+") ("something" "is" "big" "+")) -> ("something" "sees" "cat" "+"))
If something chases the cat and it sees the lion then it visits the lion.
((("something" "chases" "cat" "+") ("something" "sees" "lion" "+")) -> ("something" "visits" "lion" "+"))
If the cat chases the lion then the cat sees the lion.
((("cat" "chases" "lion" "+")) -> ("cat" "sees" "lion" "+"))
If something sees the cow and the cow sees the cat then it visits the cat.
((("something" "sees" "cow" "+") ("cow" "sees" "cat" "+")) -> ("something" "visits" "cat" "+"))
If something visits the bear then it chases the lion.
((("something" "visits" "bear" "+")) -> ("something" "chases" "lion" "+"))
If something is red then it sees the lion.
((("something" "is" "red" "+")) -> ("something" "sees" "lion" "+"))
If something visits the cat and it visits the bear then the bear is red.
((("something" "visits" "cat" "+") ("something" "visits" "bear" "+")) -> ("bear" "is" "red" "+"))
If something is big and it visits the lion then it sees the bear.
((("something" "is" "big" "+") ("something" "visits" "lion" "+")) -> ("something" "sees" "bear" "+"))
The bear chases the cat.
True
1
proof
[(triple1)]
("bear" "chases" "cat" "+")
triple1
The bear does not chase the cat.
False
1
inv-proof
[(triple1)]
("bear" "chases" "cat" "-")
triple1
The cat chases the lion.
True
2
proof
[(((triple5) -> rule5))]
("cat" "chases" "lion" "+")
((triple5) -> (rule5 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat does not chase the lion.
False
2
inv-proof
[(((triple5) -> rule5))]
("cat" "chases" "lion" "-")
((triple5) -> (rule5 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat sees the lion.
True
3
proof
[(((((triple5) -> rule5)) -> rule3))]
("cat" "sees" "lion" "+")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The cat does not see the lion.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule3))]
("cat" "sees" "lion" "-")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The bear does not see the bear.
Unknown
inv-rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "sees" "bear" "-")
The cow visits the cat.
Unknown
rconc
[@1: The cow visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "visits" "cat" "+")
The bear is not red.
Unknown
inv-rconc
[@2: The bear is red.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("bear" "is" "red" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The bear does not visit the cow.
Unknown
inv-random
[@0: The bear visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cow" "-")
The cow chases the bear.
Unknown
random
[@0: The cow chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "bear" "+")
@0: The bear chases the cat.[(triple1)] The cat chases the cow.[(triple2)] The cat is nice.[(triple3)] The cat sees the bear.[(triple4)] The cat visits the bear.[(triple5)] The cow is blue.[(triple6)] The lion sees the cat.[(triple7)] @1: The cat chases the lion.[(((triple5) -> rule5))] @2: The cat sees the lion.[(((((triple5) -> rule5)) -> rule3))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The cat chases the cow.
("cat" "chases" "cow" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat sees the bear.
("cat" "sees" "bear" "+")
triple4
The cat visits the bear.
("cat" "visits" "bear" "+")
triple5
The cow is blue.
("cow" "is" "blue" "+")
triple6
The lion sees the cat.
("lion" "sees" "cat" "+")
triple7
The cat chases the lion.
("cat" "chases" "lion" "+")
((triple5) -> (rule5 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2