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