The cat is round. The cow visits the cat. The lion needs the cat. If someone visits the cat and the cat visits the lion then the cat sees the cow. If someone is round then they visit the lion. If someone sees the cow then they need the cat.
The cat is round.
("cat" "is" "round" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If someone visits the cat and the cat visits the lion then the cat sees the cow.
((("someone" "visits" "cat" "+") ("cat" "visits" "lion" "+")) -> ("cat" "sees" "cow" "+"))
If someone is round then they visit the lion.
((("someone" "is" "round" "+")) -> ("someone" "visits" "lion" "+"))
If someone sees the cow then they need the cat.
((("someone" "sees" "cow" "+")) -> ("someone" "needs" "cat" "+"))
The lion needs the cat.
True
1
proof
[(triple3)]
("lion" "needs" "cat" "+")
triple3
The cat is not round.
False
1
inv-proof
[(triple1)]
("cat" "is" "round" "-")
triple1
The cat visits the lion.
True
2
proof
[(((triple1) -> rule2))]
("cat" "visits" "lion" "+")
((triple1) -> (rule2 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat does not visit the lion.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "visits" "lion" "-")
((triple1) -> (rule2 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat sees the cow.
True
4
proof
[(((triple2 ((triple1) -> rule2)) -> rule1))]
("cat" "sees" "cow" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat does not see the cow.
False
4
inv-proof
[(((triple2 ((triple1) -> rule2)) -> rule1))]
("cat" "sees" "cow" "-")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cow does not visit the lion.
Unknown
inv-rconc
[@1: The cow visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "lion" "-")
The cow needs the cat.
Unknown
rconc
[@1: The cow needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "cat" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "lion" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The lion sees the cat.
Unknown
random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "+")
@0: The cat is round.[(triple1)] The cow visits the cat.[(triple2)] The lion needs the cat.[(triple3)] @1: The cat visits the lion.[(((triple1) -> rule2))] @2: The cat sees the cow.[(((triple2 ((triple1) -> rule2)) -> rule1))] @3: The cat needs the cat.[(((((triple2 ((triple1) -> rule2)) -> rule1)) -> rule3))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cow visits the cat.
("cow" "visits" "cat" "+")
triple2
The lion needs the cat.
("lion" "needs" "cat" "+")
triple3
The cat visits the lion.
("cat" "visits" "lion" "+")
((triple1) -> (rule2 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
((triple2 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
((((triple2 ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3