Gary is nice. If someone is red then they are round. Quiet, red people are cold. If someone is nice then they are cold. If Gary is young and Gary is quiet then Gary is nice. All round, red people are quiet. All cold people are quiet. If someone is quiet then they are red. If Gary is round then Gary is furry.
Gary is nice.
("Gary" "is" "nice" "+")
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Quiet, red people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice then they are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If Gary is young and Gary is quiet then Gary is nice.
((("Gary" "is" "young" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "nice" "+"))
All round, red people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If Gary is round then Gary is furry.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "furry" "+"))
Gary is nice.
True
1
proof
[(triple1)]
("Gary" "is" "nice" "+")
triple1
Gary is not nice.
False
1
inv-proof
[(triple1)]
("Gary" "is" "nice" "-")
triple1
Gary is cold.
True
2
proof
[(((triple1) -> rule3))]
("Gary" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Gary" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Gary" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Gary" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule7))]
("Gary" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not red.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule7))]
("Gary" "is" "red" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
@0: Gary is nice.[(triple1)] @1: Gary is cold.[(((triple1) -> rule3))] @2: Gary is quiet.[(((((triple1) -> rule3)) -> rule6))] @3: Gary is red.[(((((((triple1) -> rule3)) -> rule6)) -> rule7))] @4: Gary is round.[(((((((((triple1) -> rule3)) -> rule6)) -> rule7)) -> rule1))] @5: Gary is furry.[(((((((((((triple1) -> rule3)) -> rule6)) -> rule7)) -> rule1)) -> rule8))]
Gary is nice.
("Gary" "is" "nice" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
((((((((((triple1) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
int5