Dave is white. White things are round. All smart, cold things are round. Round things are blue. Cold things are blue. If something is round and not furry then it is not rough. All white things are rough. Blue things are smart. If something is smart then it is cold.
Dave is white.
("Dave" "is" "white" "+")
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
All smart, cold things are round.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is round and not furry then it is not rough.
((("something" "is" "round" "+") ("something" "is" "furry" "~")) -> ("something" "is" "rough" "-"))
All white things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Dave is white.
True
1
proof
[(triple1)]
("Dave" "is" "white" "+")
triple1
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Dave is rough.
True
2
proof
[(((triple1) -> rule6))]
("Dave" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "round" "-")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Dave" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Dave" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule7))]
("Dave" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not smart.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule7))]
("Dave" "is" "smart" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
@0: Dave is white.[(triple1)] @1: Dave is rough.[(((triple1) -> rule6))] Dave is round.[(((triple1) -> rule1))] @2: Dave is blue.[(((((triple1) -> rule1)) -> rule3))] @3: Dave is smart.[(((((((triple1) -> rule1)) -> rule3)) -> rule7))] @4: Dave is cold.[(((((((((triple1) -> rule1)) -> rule3)) -> rule7)) -> rule8))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4