Dave is not cold. Dave is round. Dave is young. If Dave is smart then Dave is not kind. All smart people are round. If someone is young then they are round. If Dave is round then Dave is blue. Young, round people are smart. All kind, round people are not smart. If Dave is green then Dave is not cold. If Dave is not smart then Dave is not cold.
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
If Dave is smart then Dave is not kind.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "kind" "-"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If Dave is round then Dave is blue.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "blue" "+"))
Young, round people are smart.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All kind, round people are not smart.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "-"))
If Dave is green then Dave is not cold.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "cold" "-"))
If Dave is not smart then Dave is not cold.
((("Dave" "is" "smart" "~")) -> ("Dave" "is" "cold" "-"))
Dave is not cold.
True
1
proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
Dave is smart.
True
3
proof
[(((triple3 triple2) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5))]
("Dave" "is" "smart" "+")
((triple3 triple2) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not blue.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple3) -> rule3)) -> rule4))]
("Dave" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not kind.
True
4
proof
[(((((triple3 triple2) -> rule5)) -> rule1) OR ((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule1))]
("Dave" "is" "kind" "-")
((((triple3 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
False
4
inv-proof
[(((((triple3 triple2) -> rule5)) -> rule1) OR ((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple3 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
@0: Dave is not cold.[(triple1)] Dave is round.[(triple2 OR ((triple3) -> rule3))] Dave is young.[(triple3)] @1: Dave is blue.[(((triple2) -> rule4) OR ((((triple3) -> rule3)) -> rule4))] Dave is smart.[(((triple3 triple2) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5))] @2: Dave is not kind.[(((((triple3 triple2) -> rule5)) -> rule1) OR ((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule1))]
Dave is not cold.
("Dave" "is" "cold" "-")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
((triple3) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((triple3 triple2) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not kind.
("Dave" "is" "kind" "-")
((((triple3 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3