Dave is cold. Dave is quiet. Dave is round. Dave is smart. Gary is nice. Gary is quiet. Gary is red. Gary is round. Gary is smart. Gary is white. All cold, red things are quiet. White, smart things are red. White things are smart. If Gary is smart and Gary is red then Gary is white. All quiet things are white. White things are red. If Dave is smart and Dave is red then Dave is nice. If Dave is nice and Dave is cold then Dave is quiet.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
All cold, red things are quiet.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
White, smart things are red.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
White things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Gary is smart and Gary is red then Gary is white.
((("Gary" "is" "smart" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "white" "+"))
All quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
White things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If Dave is smart and Dave is red then Dave is nice.
((("Dave" "is" "smart" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "nice" "+"))
If Dave is nice and Dave is cold then Dave is quiet.
((("Dave" "is" "nice" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "quiet" "+"))
Gary is white.
True
1
proof
[(triple10 OR ((triple6) -> rule5) OR ((triple9 triple7) -> rule4))]
("Gary" "is" "white" "+")
triple10
((triple6) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple9 triple7) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is not smart.
False
1
inv-proof
[(triple4 OR ((((triple2) -> rule5)) -> rule3))]
("Dave" "is" "smart" "-")
triple4
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is white.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "white" "+")
((triple2) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "white" "-")
((triple2) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
True
3
proof
[(((((triple2) -> rule5)) -> rule6) OR ((((triple2) -> rule5) triple4) -> rule2) OR ((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule3)) -> rule2))]
("Dave" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not red.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6) OR ((((triple2) -> rule5) triple4) -> rule2) OR ((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule3)) -> rule2))]
("Dave" "is" "red" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
True
5
proof
[(((triple4 ((((triple2) -> rule5)) -> rule6)) -> rule7) OR ((triple4 ((((triple2) -> rule5) triple4) -> rule2)) -> rule7) OR ((((((triple2) -> rule5)) -> rule3) ((((triple2) -> rule5)) -> rule6)) -> rule7) OR ((((((triple2) -> rule5)) -> rule3) ((((triple2) -> rule5) triple4) -> rule2)) -> rule7) OR ((triple4 ((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule3)) -> rule2)) -> rule7) OR ((((((triple2) -> rule5)) -> rule3) ((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule3)) -> rule2)) -> rule7))]
("Dave" "is" "nice" "+")
((triple4 ((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((triple4 ((((triple2) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple2) -> (rule5 % int4))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple2) -> (rule5 % int4)) triple4) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((triple4 ((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is not nice.
False
5
inv-proof
[(((triple4 ((((triple2) -> rule5)) -> rule6)) -> rule7) OR ((triple4 ((((triple2) -> rule5) triple4) -> rule2)) -> rule7) OR ((((((triple2) -> rule5)) -> rule3) ((((triple2) -> rule5)) -> rule6)) -> rule7) OR ((((((triple2) -> rule5)) -> rule3) ((((triple2) -> rule5) triple4) -> rule2)) -> rule7) OR ((triple4 ((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule3)) -> rule2)) -> rule7) OR ((((((triple2) -> rule5)) -> rule3) ((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule3)) -> rule2)) -> rule7))]
("Dave" "is" "nice" "-")
((triple4 ((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((triple4 ((((triple2) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple2) -> (rule5 % int4))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple2) -> (rule5 % int4)) triple4) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((triple4 ((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
@0: Dave is cold.[(triple1)] Dave is quiet.[(triple2)] Dave is round.[(triple3)] Dave is smart.[(triple4 OR ((((triple2) -> rule5)) -> rule3))] Gary is nice.[(triple5)] Gary is quiet.[(triple6)] Gary is red.[(triple7 OR ((triple10) -> rule6) OR ((triple10 triple9) -> rule2) OR ((((triple6) -> rule5)) -> rule6) OR ((triple10 ((triple10) -> rule3)) -> rule2) OR ((((triple6) -> rule5) triple9) -> rule2) OR ((((triple6) -> rule5) ((triple10) -> rule3)) -> rule2) OR ((triple10 ((((triple6) -> rule5)) -> rule3)) -> rule2) OR ((((triple6) -> rule5) ((((triple6) -> rule5)) -> rule3)) -> rule2))] Gary is round.[(triple8)] Gary is smart.[(triple9 OR ((triple10) -> rule3) OR ((((triple6) -> rule5)) -> rule3))] Gary is white.[(triple10 OR ((triple6) -> rule5) OR ((triple9 triple7) -> rule4))] @1: Dave is white.[(((triple2) -> rule5))] @2: Dave is red.[(((((triple2) -> rule5)) -> rule6) OR ((((triple2) -> rule5) triple4) -> rule2) OR ((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule3)) -> rule2))] @3: Dave is nice.[(((triple4 ((((triple2) -> rule5)) -> rule6)) -> rule7) OR ((triple4 ((((triple2) -> rule5) triple4) -> rule2)) -> rule7) OR ((((((triple2) -> rule5)) -> rule3) ((((triple2) -> rule5)) -> rule6)) -> rule7) OR ((((((triple2) -> rule5)) -> rule3) ((((triple2) -> rule5) triple4) -> rule2)) -> rule7) OR ((triple4 ((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule3)) -> rule2)) -> rule7) OR ((((((triple2) -> rule5)) -> rule3) ((((triple2) -> rule5) ((((triple2) -> rule5)) -> rule3)) -> rule2)) -> rule7))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
((triple10) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple10 triple9) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((triple10 ((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple6) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple6) -> (rule5 % int3)) ((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((triple10 ((((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((triple6) -> (rule5 % int3)) ((((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
((triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple10
((triple6) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple9 triple7) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple2) -> (rule5 % int3)) ((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((triple4 ((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((triple4 ((((triple2) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple2) -> (rule5 % int4))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple2) -> (rule5 % int4)) triple4) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((triple4 ((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4