The tiger is green. All rough things are green. All red, green things are blue. All blue, big things are red. If something is blue and red then it is rough. If the tiger is rough and the tiger is blue then the tiger is green. All big things are red. Green things are big. If something is blue and red then it is rough.
The tiger is green.
("tiger" "is" "green" "+")
All rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
All red, green things are blue.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All blue, big things are red.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is blue and red then it is rough.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If the tiger is rough and the tiger is blue then the tiger is green.
((("tiger" "is" "rough" "+") ("tiger" "is" "blue" "+")) -> ("tiger" "is" "green" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is blue and red then it is rough.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
The tiger is green.
True
1
proof
[(triple1)]
("tiger" "is" "green" "+")
triple1
The tiger is not green.
False
1
inv-proof
[(triple1)]
("tiger" "is" "green" "-")
triple1
The tiger is big.
True
2
proof
[(((triple1) -> rule7))]
("tiger" "is" "big" "+")
((triple1) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not big.
False
2
inv-proof
[(((triple1) -> rule7))]
("tiger" "is" "big" "-")
((triple1) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
True
3
proof
[(((((triple1) -> rule7)) -> rule6))]
("tiger" "is" "red" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is not red.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule6))]
("tiger" "is" "red" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
True
5
proof
[(((((((triple1) -> rule7)) -> rule6) triple1) -> rule2))]
("tiger" "is" "blue" "+")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is not blue.
False
5
inv-proof
[(((((((triple1) -> rule7)) -> rule6) triple1) -> rule2))]
("tiger" "is" "blue" "-")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "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 green.[(triple1)] @1: The tiger is big.[(((triple1) -> rule7))] @2: The tiger is red.[(((((triple1) -> rule7)) -> rule6))] @3: The tiger is blue.[(((((((triple1) -> rule7)) -> rule6) triple1) -> rule2))] @4: The tiger is rough.[(((((((((triple1) -> rule7)) -> rule6) triple1) -> rule2) ((((triple1) -> rule7)) -> rule6)) -> rule4) OR ((((((((triple1) -> rule7)) -> rule6) triple1) -> rule2) ((((triple1) -> rule7)) -> rule6)) -> rule8))]
The tiger is green.
("tiger" "is" "green" "+")
triple1
The tiger is big.
("tiger" "is" "big" "+")
((triple1) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3)) triple1) -> (rule2 % int2)) ((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
((((((((triple1) -> (rule7 % int4))) -> (rule6 % int3)) triple1) -> (rule2 % int2)) ((((triple1) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4