The tiger is big. Cold, young people are rough. If someone is young then they are nice. If the tiger is big then the tiger is young. If someone is young then they are nice. Cold, big people are nice. All young people are cold. All rough, cold people are young. If the tiger is young and the tiger is nice then the tiger is big.
The tiger is big.
("tiger" "is" "big" "+")
Cold, young people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If the tiger is big then the tiger is young.
((("tiger" "is" "big" "+")) -> ("tiger" "is" "young" "+"))
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Cold, big people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All rough, cold people are young.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If the tiger is young and the tiger is nice then the tiger is big.
((("tiger" "is" "young" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "is" "big" "+"))
The tiger is big.
True
1
proof
[(triple1)]
("tiger" "is" "big" "+")
triple1
The tiger is not big.
False
1
inv-proof
[(triple1)]
("tiger" "is" "big" "-")
triple1
The tiger is young.
True
2
proof
[(((triple1) -> rule3))]
("tiger" "is" "young" "+")
((triple1) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("tiger" "is" "young" "-")
((triple1) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule3)) -> rule4) OR ((((((triple1) -> rule3)) -> rule6) triple1) -> rule5))]
("tiger" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) triple1) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is not cold.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("tiger" "is" "cold" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is rough.
True
6
proof
[(((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule1))]
("tiger" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is not rough.
False
6
inv-proof
[(((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule1))]
("tiger" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The tiger is big.[(triple1)] @1: The tiger is young.[(((triple1) -> rule3))] @2: The tiger is cold.[(((((triple1) -> rule3)) -> rule6))] The tiger is nice.[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule3)) -> rule4) OR ((((((triple1) -> rule3)) -> rule6) triple1) -> rule5))] @3: The tiger is rough.[(((((((triple1) -> rule3)) -> rule6) ((triple1) -> rule3)) -> rule1))]
The tiger is big.
("tiger" "is" "big" "+")
triple1
The tiger is young.
("tiger" "is" "young" "+")
((triple1) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) triple1) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3