Dave is blue. Dave is red. Dave is smart. All cold things are rough. If something is red then it is blue. All blue, smart things are red. Rough, blue things are round. Smart, blue things are cold. Blue things are red.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All blue, smart things are red.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Rough, blue things are round.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Smart, blue things are cold.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Dave is red.
True
1
proof
[(triple2 OR ((triple1) -> rule6) OR ((triple1 triple3) -> rule3))]
("Dave" "is" "red" "+")
triple2
((triple1) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple1 triple3) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule6) OR ((triple1 triple3) -> rule3))]
("Dave" "is" "red" "-")
triple2
((triple1) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple1 triple3) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
True
3
proof
[(((triple3 triple1) -> rule5) OR ((triple3 ((triple2) -> rule2)) -> rule5))]
("Dave" "is" "cold" "+")
((triple3 triple1) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((triple3 triple1) -> rule5) OR ((triple3 ((triple2) -> rule2)) -> rule5))]
("Dave" "is" "cold" "-")
((triple3 triple1) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
True
4
proof
[(((((triple3 triple1) -> rule5)) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule1))]
("Dave" "is" "rough" "+")
((((triple3 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not rough.
False
4
inv-proof
[(((((triple3 triple1) -> rule5)) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule1))]
("Dave" "is" "rough" "-")
((((triple3 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
True
6
proof
[(((((((triple3 triple1) -> rule5)) -> rule1) triple1) -> rule4) OR ((((((triple3 triple1) -> rule5)) -> rule1) ((triple2) -> rule2)) -> rule4) OR ((((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule1) triple1) -> rule4) OR ((((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule1) ((triple2) -> rule2)) -> rule4))]
("Dave" "is" "round" "+")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple3 triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2) -> (rule2 % int4))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not round.
False
6
inv-proof
[(((((((triple3 triple1) -> rule5)) -> rule1) triple1) -> rule4) OR ((((((triple3 triple1) -> rule5)) -> rule1) ((triple2) -> rule2)) -> rule4) OR ((((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule1) triple1) -> rule4) OR ((((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule1) ((triple2) -> rule2)) -> rule4))]
("Dave" "is" "round" "-")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple3 triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2) -> (rule2 % int4))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
@0: Dave is blue.[(triple1 OR ((triple2) -> rule2))] Dave is red.[(triple2 OR ((triple1) -> rule6) OR ((triple1 triple3) -> rule3))] Dave is smart.[(triple3)] @1: Dave is cold.[(((triple3 triple1) -> rule5) OR ((triple3 ((triple2) -> rule2)) -> rule5))] @2: Dave is rough.[(((((triple3 triple1) -> rule5)) -> rule1) OR ((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule1))] @3: Dave is round.[(((((((triple3 triple1) -> rule5)) -> rule1) triple1) -> rule4) OR ((((((triple3 triple1) -> rule5)) -> rule1) ((triple2) -> rule2)) -> rule4) OR ((((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule1) triple1) -> rule4) OR ((((((triple3 ((triple2) -> rule2)) -> rule5)) -> rule1) ((triple2) -> rule2)) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple2
((triple1) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple1 triple3) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple3 triple1) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple3 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple3 triple1) -> (rule5 % int4))) -> (rule1 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
((((((triple3 ((triple2) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2) -> (rule2 % int4))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4