The cat likes the tiger. The tiger is not round. The tiger likes the cat. If something is rough and it likes the cat then the cat sees the tiger. If something is big and it does not like the cat then the cat eats the tiger. If something likes the cat then the cat is blue.
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The tiger is not round.
("tiger" "is" "round" "-")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If something is rough and it likes the cat then the cat sees the tiger.
((("something" "is" "rough" "+") ("something" "likes" "cat" "+")) -> ("cat" "sees" "tiger" "+"))
If something is big and it does not like the cat then the cat eats the tiger.
((("something" "is" "big" "+") ("something" "likes" "cat" "~")) -> ("cat" "eats" "tiger" "+"))
If something likes the cat then the cat is blue.
((("something" "likes" "cat" "+")) -> ("cat" "is" "blue" "+"))
The tiger likes the cat.
True
1
proof
[(triple3)]
("tiger" "likes" "cat" "+")
triple3
The tiger is round.
False
1
inv-proof
[(triple2)]
("tiger" "is" "round" "+")
triple2
The cat is blue.
True
2
proof
[(((triple3) -> rule3))]
("cat" "is" "blue" "+")
((triple3) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is not blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("cat" "is" "blue" "-")
((triple3) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat does not eat the tiger.
Unknown
inv-rconc
[@1: The cat eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "tiger" "-")
The cat sees the tiger.
Unknown
rconc
[@1: The cat sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "tiger" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
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 likes the tiger.[(triple1)] The tiger is not round.[(triple2)] The tiger likes the cat.[(triple3)] @1: The cat is blue.[(((triple3) -> rule3))]
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple1
The tiger is not round.
("tiger" "is" "round" "-")
triple2
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple3
The cat is blue.
("cat" "is" "blue" "+")
((triple3) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1