The cat eats the tiger. The cat is green. The cat is kind. The cat sees the tiger. The tiger eats the cat. The tiger is kind. The tiger is red. The tiger is round. The tiger sees the cat. The tiger visits the cat. If something visits the tiger and it eats the cat then the tiger visits the cat. If something visits the cat then the cat is round. If something is round then it visits the tiger.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something visits the tiger and it eats the cat then the tiger visits the cat.
((("something" "visits" "tiger" "+") ("something" "eats" "cat" "+")) -> ("tiger" "visits" "cat" "+"))
If something visits the cat then the cat is round.
((("something" "visits" "cat" "+")) -> ("cat" "is" "round" "+"))
If something is round then it visits the tiger.
((("something" "is" "round" "+")) -> ("something" "visits" "tiger" "+"))
The cat sees the tiger.
True
1
proof
[(triple4)]
("cat" "sees" "tiger" "+")
triple4
The tiger is not round.
False
1
inv-proof
[(triple8)]
("tiger" "is" "round" "-")
triple8
The cat is round.
True
2
proof
[(((triple10) -> rule2) OR ((((((triple8) -> rule3) triple5) -> rule1)) -> rule2))]
("cat" "is" "round" "+")
((triple10) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((((((triple8) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The cat is not round.
False
2
inv-proof
[(((triple10) -> rule2) OR ((((((triple8) -> rule3) triple5) -> rule1)) -> rule2))]
("cat" "is" "round" "-")
((triple10) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((((((triple8) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The cat visits the tiger.
True
3
proof
[(((((triple10) -> rule2)) -> rule3) OR ((((((((triple8) -> rule3) triple5) -> rule1)) -> rule2)) -> rule3))]
("cat" "visits" "tiger" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((((((triple8) -> (rule3 % int4)) triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4
The cat does not visit the tiger.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule3) OR ((((((((triple8) -> rule3) triple5) -> rule1)) -> rule2)) -> rule3))]
("cat" "visits" "tiger" "-")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((((((triple8) -> (rule3 % int4)) triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat eats the tiger.[(triple1)] The cat is green.[(triple2)] The cat is kind.[(triple3)] The cat sees the tiger.[(triple4)] The tiger eats the cat.[(triple5)] The tiger is kind.[(triple6)] The tiger is red.[(triple7)] The tiger is round.[(triple8)] The tiger sees the cat.[(triple9)] The tiger visits the cat.[(triple10 OR ((((triple8) -> rule3) triple5) -> rule1))] @1: The cat is round.[(((triple10) -> rule2) OR ((((((triple8) -> rule3) triple5) -> rule1)) -> rule2))] The tiger visits the tiger.[(((triple8) -> rule3))] @2: The cat visits the tiger.[(((((triple10) -> rule2)) -> rule3) OR ((((((((triple8) -> rule3) triple5) -> rule1)) -> rule2)) -> rule3))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger is red.
("tiger" "is" "red" "+")
triple7
The tiger is round.
("tiger" "is" "round" "+")
triple8
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple9
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
((((triple8) -> (rule3 % int2)) triple5) -> (rule1 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((triple10) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((((((triple8) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple8) -> (rule3 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((((((triple8) -> (rule3 % int4)) triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int4