The tiger is young. If something is green and young then it is blue. Nice things are green. If something is young then it is nice. Young things are nice. Green things are young. All nice, green things are young. If the tiger is blue then the tiger is red. If the tiger is young and the tiger is not nice then the tiger is blue.
The tiger is young.
("tiger" "is" "young" "+")
If something is green and young then it is blue.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All nice, green things are young.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If the tiger is blue then the tiger is red.
((("tiger" "is" "blue" "+")) -> ("tiger" "is" "red" "+"))
If the tiger is young and the tiger is not nice then the tiger is blue.
((("tiger" "is" "young" "+") ("tiger" "is" "nice" "~")) -> ("tiger" "is" "blue" "+"))
The tiger is young.
True
1
proof
[(triple1)]
("tiger" "is" "young" "+")
triple1
The tiger is not young.
False
1
inv-proof
[(triple1)]
("tiger" "is" "young" "-")
triple1
The tiger is nice.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("tiger" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((triple1) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not nice.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("tiger" "is" "nice" "-")
((triple1) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((triple1) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is green.
True
3
proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule4)) -> rule2))]
("tiger" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is not green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule4)) -> rule2))]
("tiger" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is blue.
True
5
proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule1) OR ((((((triple1) -> rule4)) -> rule2) triple1) -> rule1))]
("tiger" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is not blue.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule1) OR ((((((triple1) -> rule4)) -> rule2) triple1) -> rule1))]
("tiger" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The tiger is young.[(triple1)] @1: The tiger is nice.[(((triple1) -> rule3) OR ((triple1) -> rule4))] @2: The tiger is green.[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule4)) -> rule2))] @3: The tiger is blue.[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule1) OR ((((((triple1) -> rule4)) -> rule2) triple1) -> rule1))] @4: The tiger is red.[(((((((((triple1) -> rule3)) -> rule2) triple1) -> rule1)) -> rule7) OR ((((((((triple1) -> rule4)) -> rule2) triple1) -> rule1)) -> rule7))]
The tiger is young.
("tiger" "is" "young" "+")
triple1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((triple1) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
((((((((triple1) -> (rule4 % int4))) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4