The tiger is nice. All young things are big. All young, blue things are red. Big, young things are blue. If the tiger is nice and the tiger is blue then the tiger is young. All nice things are young. Nice, big things are blue. All blue, red things are young. All blue, young things are big.
The tiger is nice.
("tiger" "is" "nice" "+")
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All young, blue things are red.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Big, young things are blue.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If the tiger is nice and the tiger is blue then the tiger is young.
((("tiger" "is" "nice" "+") ("tiger" "is" "blue" "+")) -> ("tiger" "is" "young" "+"))
All nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Nice, big things are blue.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All blue, red things are young.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All blue, young things are big.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
The tiger is nice.
True
1
proof
[(triple1)]
("tiger" "is" "nice" "+")
triple1
The tiger is not nice.
False
1
inv-proof
[(triple1)]
("tiger" "is" "nice" "-")
triple1
The tiger is young.
True
2
proof
[(((triple1) -> rule5))]
("tiger" "is" "young" "+")
((triple1) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is not young.
False
2
inv-proof
[(((triple1) -> rule5))]
("tiger" "is" "young" "-")
((triple1) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("tiger" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is not big.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("tiger" "is" "big" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is blue.
True
5
proof
[(((triple1 ((((triple1) -> rule5)) -> rule1)) -> rule6) OR ((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule3))]
("tiger" "is" "blue" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is not blue.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule5)) -> rule1)) -> rule6) OR ((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule3))]
("tiger" "is" "blue" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
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 likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The tiger is nice.[(triple1)] @1: The tiger is young.[(((triple1) -> rule5))] @2: The tiger is big.[(((((triple1) -> rule5)) -> rule1))] @3: The tiger is blue.[(((triple1 ((((triple1) -> rule5)) -> rule1)) -> rule6) OR ((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule3))] @4: The tiger is red.[(((((triple1) -> rule5) ((triple1 ((((triple1) -> rule5)) -> rule1)) -> rule6)) -> rule2) OR ((((triple1) -> rule5) ((((((triple1) -> rule5)) -> rule1) ((triple1) -> rule5)) -> rule3)) -> rule2))]
The tiger is nice.
("tiger" "is" "nice" "+")
triple1
The tiger is young.
("tiger" "is" "young" "+")
((triple1) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule5 % int3))) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
((((triple1) -> (rule5 % int4)) ((triple1 ((((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is young.
("tiger" "is" "young" "+")
int4
((((triple1) -> (rule5 % int4)) ((((((triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple1) -> (rule5 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is young.
("tiger" "is" "young" "+")
int4