Gary is big. If Gary is white then Gary is round. If someone is red then they are quiet. All big people are white. If someone is nice and red then they are big. Cold, round people are big. Round people are red.
Gary is big.
("Gary" "is" "big" "+")
If Gary is white then Gary is round.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "round" "+"))
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is nice and red then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Cold, round people are big.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Gary is big.
True
1
proof
[(triple1)]
("Gary" "is" "big" "+")
triple1
Gary is not big.
False
1
inv-proof
[(triple1)]
("Gary" "is" "big" "-")
triple1
Gary is white.
True
2
proof
[(((triple1) -> rule3))]
("Gary" "is" "white" "+")
((triple1) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Gary" "is" "white" "-")
((triple1) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Gary" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Gary" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule6))]
("Gary" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not red.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule6))]
("Gary" "is" "red" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Gary is big.[(triple1)] @1: Gary is white.[(((triple1) -> rule3))] @2: Gary is round.[(((((triple1) -> rule3)) -> rule1))] @3: Gary is red.[(((((((triple1) -> rule3)) -> rule1)) -> rule6))] @4: Gary is quiet.[(((((((((triple1) -> rule3)) -> rule1)) -> rule6)) -> rule2))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
((triple1) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4