The cat is blue. The cat is rough. The cat sees the tiger. The cat visits the tiger. The tiger eats the cat. The tiger is green. The tiger is round. If the tiger eats the cat then the tiger visits the cat. If the tiger eats the cat and the tiger visits the cat then the tiger is rough. If someone sees the cat then they are round.
The cat is blue.
("cat" "is" "blue" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is round.
("tiger" "is" "round" "+")
If the tiger eats the cat then the tiger visits the cat.
((("tiger" "eats" "cat" "+")) -> ("tiger" "visits" "cat" "+"))
If the tiger eats the cat and the tiger visits the cat then the tiger is rough.
((("tiger" "eats" "cat" "+") ("tiger" "visits" "cat" "+")) -> ("tiger" "is" "rough" "+"))
If someone sees the cat then they are round.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "round" "+"))
The cat is rough.
True
1
proof
[(triple2)]
("cat" "is" "rough" "+")
triple2
The cat does not see the tiger.
False
1
inv-proof
[(triple3)]
("cat" "sees" "tiger" "-")
triple3
The tiger visits the cat.
True
2
proof
[(((triple5) -> rule1))]
("tiger" "visits" "cat" "+")
((triple5) -> (rule1 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger does not visit the cat.
False
2
inv-proof
[(((triple5) -> rule1))]
("tiger" "visits" "cat" "-")
((triple5) -> (rule1 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger is rough.
True
4
proof
[(((triple5 ((triple5) -> rule1)) -> rule2))]
("tiger" "is" "rough" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger is not rough.
False
4
inv-proof
[(((triple5 ((triple5) -> rule1)) -> rule2))]
("tiger" "is" "rough" "-")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "round" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
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 is blue.[(triple1)] The cat is rough.[(triple2)] The cat sees the tiger.[(triple3)] The cat visits the tiger.[(triple4)] The tiger eats the cat.[(triple5)] The tiger is green.[(triple6)] The tiger is round.[(triple7)] @1: The tiger visits the cat.[(((triple5) -> rule1))] @2: The tiger is rough.[(((triple5 ((triple5) -> rule1)) -> rule2))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple4
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple5
The tiger is green.
("tiger" "is" "green" "+")
triple6
The tiger is round.
("tiger" "is" "round" "+")
triple7
The tiger visits the cat.
("tiger" "visits" "cat" "+")
((triple5) -> (rule1 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2