The cat eats the lion. The cat is green. The cat sees the lion. The cat sees the tiger. The cat visits the tiger. The lion eats the cat. The lion sees the cat. The lion sees the tiger. The lion visits the tiger. The tiger is rough. The tiger sees the lion. The tiger does not visit the lion. If something is red then it eats the lion. If the tiger is big then the tiger does not visit the lion. If something eats the lion then it is big.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is green.
("cat" "is" "green" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger does not visit the lion.
("tiger" "visits" "lion" "-")
If something is red then it eats the lion.
((("something" "is" "red" "+")) -> ("something" "eats" "lion" "+"))
If the tiger is big then the tiger does not visit the lion.
((("tiger" "is" "big" "+")) -> ("tiger" "visits" "lion" "-"))
If something eats the lion then it is big.
((("something" "eats" "lion" "+")) -> ("something" "is" "big" "+"))
The lion visits the tiger.
True
1
proof
[(triple9)]
("lion" "visits" "tiger" "+")
triple9
The cat does not eat the lion.
False
1
inv-proof
[(triple1)]
("cat" "eats" "lion" "-")
triple1
The cat is big.
True
2
proof
[(((triple1) -> rule3))]
("cat" "is" "big" "+")
((triple1) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "is" "big" "-")
((triple1) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The tiger does not eat the lion.
Unknown
inv-rconc
[@1: The tiger eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "lion" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "lion" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cat eats the lion.[(triple1)] The cat is green.[(triple2)] The cat sees the lion.[(triple3)] The cat sees the tiger.[(triple4)] The cat visits the tiger.[(triple5)] The lion eats the cat.[(triple6)] The lion sees the cat.[(triple7)] The lion sees the tiger.[(triple8)] The lion visits the tiger.[(triple9)] The tiger does not visit the lion.[(triple12)] The tiger is rough.[(triple10)] The tiger sees the lion.[(triple11)] @1: The cat is big.[(((triple1) -> rule3))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat sees the lion.
("cat" "sees" "lion" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple5
The lion eats the cat.
("lion" "eats" "cat" "+")
triple6
The lion sees the cat.
("lion" "sees" "cat" "+")
triple7
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple8
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple9
The tiger does not visit the lion.
("tiger" "visits" "lion" "-")
triple12
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple11
The cat is big.
("cat" "is" "big" "+")
((triple1) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1