The tiger is round. Nice, round things are green. Round, nice things are green. If something is nice and blue then it is not green. If something is round then it is nice. Green things are young. If the tiger is not green then the tiger is young.
The tiger is round.
("tiger" "is" "round" "+")
Nice, round things are green.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Round, nice things are green.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is nice and blue then it is not green.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
If something is round then it is nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If the tiger is not green then the tiger is young.
((("tiger" "is" "green" "~")) -> ("tiger" "is" "young" "+"))
The tiger is round.
True
1
proof
[(triple1)]
("tiger" "is" "round" "+")
triple1
The tiger is not round.
False
1
inv-proof
[(triple1)]
("tiger" "is" "round" "-")
triple1
The tiger is nice.
True
2
proof
[(((triple1) -> rule4))]
("tiger" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("tiger" "is" "nice" "-")
((triple1) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is green.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule2) OR ((((triple1) -> rule4) triple1) -> rule1))]
("tiger" "is" "green" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is not green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule2) OR ((((triple1) -> rule4) triple1) -> rule1))]
("tiger" "is" "green" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is young.
True
5
proof
[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule5) OR ((((((triple1) -> rule4) triple1) -> rule1)) -> rule5))]
("tiger" "is" "young" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is not young.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule5) OR ((((((triple1) -> rule4) triple1) -> rule1)) -> rule5))]
("tiger" "is" "young" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
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 eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The tiger is round.[(triple1)] @1: The tiger is nice.[(((triple1) -> rule4))] @2: The tiger is green.[(((triple1 ((triple1) -> rule4)) -> rule2) OR ((((triple1) -> rule4) triple1) -> rule1))] @3: The tiger is young.[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule5) OR ((((((triple1) -> rule4) triple1) -> rule1)) -> rule5))]
The tiger is round.
("tiger" "is" "round" "+")
triple1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3