The tiger is round. If someone is blue and big then they are round. All round people are blue. If someone is blue then they are big. Big people are cold. If the tiger is blue and the tiger is not kind then the tiger is cold. If the tiger is not big and the tiger is not blue then the tiger is cold.
The tiger is round.
("tiger" "is" "round" "+")
If someone is blue and big then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If the tiger is blue and the tiger is not kind then the tiger is cold.
((("tiger" "is" "blue" "+") ("tiger" "is" "kind" "~")) -> ("tiger" "is" "cold" "+"))
If the tiger is not big and the tiger is not blue then the tiger is cold.
((("tiger" "is" "big" "~") ("tiger" "is" "blue" "~")) -> ("tiger" "is" "cold" "+"))
The tiger is round.
True
1
proof
[(triple1)]
("tiger" "is" "round" "+")
triple1
The tiger is not round.
False
1
inv-proof
[(triple1)]
("tiger" "is" "round" "-")
triple1
The tiger is blue.
True
2
proof
[(((triple1) -> rule2))]
("tiger" "is" "blue" "+")
((triple1) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("tiger" "is" "blue" "-")
((triple1) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("tiger" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is not big.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("tiger" "is" "big" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is cold.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
("tiger" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The tiger is not cold.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
("tiger" "is" "cold" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
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 round.[(triple1)] @1: The tiger is blue.[(((triple1) -> rule2))] @2: The tiger is big.[(((((triple1) -> rule2)) -> rule3))] @3: The tiger is cold.[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
The tiger is round.
("tiger" "is" "round" "+")
triple1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple1) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3