Dave is cold. Dave is kind. Dave is quiet. All white people are not round. If someone is quiet and blue then they are round. If Dave is white and Dave is cold then Dave is quiet. If Dave is quiet then Dave is round. White people are cold. If Dave is quiet then Dave is blue. All blue, cold people are not big. If someone is quiet and white then they are big.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
All white people are not round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "-"))
If someone is quiet and blue then they are round.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If Dave is white and Dave is cold then Dave is quiet.
((("Dave" "is" "white" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "quiet" "+"))
If Dave is quiet then Dave is round.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "round" "+"))
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Dave is quiet then Dave is blue.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "blue" "+"))
All blue, cold people are not big.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "-"))
If someone is quiet and white then they are big.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Dave is cold.
True
1
proof
[(triple1)]
("Dave" "is" "cold" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Dave is blue.
True
2
proof
[(((triple3) -> rule6))]
("Dave" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple3) -> rule6))]
("Dave" "is" "blue" "-")
((triple3) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not big.
True
4
proof
[(((((triple3) -> rule6) triple1) -> rule7))]
("Dave" "is" "big" "-")
((((triple3) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is big.
False
4
inv-proof
[(((((triple3) -> rule6) triple1) -> rule7))]
("Dave" "is" "big" "+")
((((triple3) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
@0: Dave is cold.[(triple1)] Dave is kind.[(triple2)] Dave is quiet.[(triple3)] @1: Dave is blue.[(((triple3) -> rule6))] Dave is round.[(((triple3) -> rule4) OR ((triple3 ((triple3) -> rule6)) -> rule2))] @2: Dave is not big.[(((((triple3) -> rule6) triple1) -> rule7))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple3 ((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
((((triple3) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2