The tiger is blue. The tiger is round. The tiger is young. All green, big things are young. Round things are green. All green, round things are big. All green, round things are big. If something is big then it is blue. If something is big and not round then it is not blue. If the tiger is big and the tiger is round then the tiger is young. If the tiger is green then the tiger is blue.
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
All green, big things are young.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All green, round things are big.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All green, round things are big.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is big and not round then it is not blue.
((("something" "is" "big" "+") ("something" "is" "round" "~")) -> ("something" "is" "blue" "-"))
If the tiger is big and the tiger is round then the tiger is young.
((("tiger" "is" "big" "+") ("tiger" "is" "round" "+")) -> ("tiger" "is" "young" "+"))
If the tiger is green then the tiger is blue.
((("tiger" "is" "green" "+")) -> ("tiger" "is" "blue" "+"))
The tiger is young.
True
1
proof
[(triple3 OR ((((((triple2) -> rule2) triple2) -> rule3) triple2) -> rule7) OR ((((((triple2) -> rule2) triple2) -> rule4) triple2) -> rule7) OR ((((triple2) -> rule2) ((((triple2) -> rule2) triple2) -> rule3)) -> rule1) OR ((((triple2) -> rule2) ((((triple2) -> rule2) triple2) -> rule4)) -> rule1))]
("tiger" "is" "young" "+")
triple3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule7 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule4 % int2)) triple2) -> (rule7 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is not young.
False
1
inv-proof
[(triple3 OR ((((((triple2) -> rule2) triple2) -> rule3) triple2) -> rule7) OR ((((((triple2) -> rule2) triple2) -> rule4) triple2) -> rule7) OR ((((triple2) -> rule2) ((((triple2) -> rule2) triple2) -> rule3)) -> rule1) OR ((((triple2) -> rule2) ((((triple2) -> rule2) triple2) -> rule4)) -> rule1))]
("tiger" "is" "young" "-")
triple3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule7 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule4 % int2)) triple2) -> (rule7 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is green.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "is" "green" "+")
((triple2) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "is" "green" "-")
((triple2) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is big.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule3) OR ((((triple2) -> rule2) triple2) -> rule4))]
("tiger" "is" "big" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((triple2) -> (rule2 % int2)) triple2) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is not big.
False
4
inv-proof
[(((((triple2) -> rule2) triple2) -> rule3) OR ((((triple2) -> rule2) triple2) -> rule4))]
("tiger" "is" "big" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((triple2) -> (rule2 % int2)) triple2) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
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 needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The tiger is blue.[(triple1 OR ((((triple2) -> rule2)) -> rule8) OR ((((((triple2) -> rule2) triple2) -> rule3)) -> rule5) OR ((((((triple2) -> rule2) triple2) -> rule4)) -> rule5))] The tiger is round.[(triple2)] The tiger is young.[(triple3 OR ((((((triple2) -> rule2) triple2) -> rule3) triple2) -> rule7) OR ((((((triple2) -> rule2) triple2) -> rule4) triple2) -> rule7) OR ((((triple2) -> rule2) ((((triple2) -> rule2) triple2) -> rule3)) -> rule1) OR ((((triple2) -> rule2) ((((triple2) -> rule2) triple2) -> rule4)) -> rule1))] @1: The tiger is green.[(((triple2) -> rule2))] @2: The tiger is big.[(((((triple2) -> rule2) triple2) -> rule3) OR ((((triple2) -> rule2) triple2) -> rule4))]
The tiger is blue.
("tiger" "is" "blue" "+")
triple1
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((((triple2) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
triple2
The tiger is young.
("tiger" "is" "young" "+")
triple3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule7 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule4 % int2)) triple2) -> (rule7 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
((triple2) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((triple2) -> (rule2 % int2)) triple2) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2