Dave is cold. Dave is furry. Dave is round. Dave is smart. Dave is white. Dave is young. Gary is furry. Gary is round. Gary is white. Gary is young. All white people are nice. White, nice people are young. Nice, young people are cold.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All white people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
White, nice people are young.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Nice, young people are cold.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Dave is smart.
True
1
proof
[(triple4)]
("Dave" "is" "smart" "+")
triple4
Dave is not round.
False
1
inv-proof
[(triple3)]
("Dave" "is" "round" "-")
triple3
Dave is nice.
True
2
proof
[(((triple5) -> rule1))]
("Dave" "is" "nice" "+")
((triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple9) -> rule1))]
("Gary" "is" "nice" "-")
((triple9) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
True
4
proof
[(((((triple9) -> rule1) triple10) -> rule3) OR ((((triple9) -> rule1) ((triple9 ((triple9) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "cold" "+")
((((triple9) -> (rule1 % int2)) triple10) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple9) -> (rule1 % int3)) ((triple9 ((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not cold.
False
4
inv-proof
[(((((triple9) -> rule1) triple10) -> rule3) OR ((((triple9) -> rule1) ((triple9 ((triple9) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "cold" "-")
((((triple9) -> (rule1 % int2)) triple10) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple9) -> (rule1 % int3)) ((triple9 ((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
@0: Dave is cold.[(triple1 OR ((((triple5) -> rule1) triple6) -> rule3) OR ((((triple5) -> rule1) ((triple5 ((triple5) -> rule1)) -> rule2)) -> rule3))] Dave is furry.[(triple2)] Dave is round.[(triple3)] Dave is smart.[(triple4)] Dave is white.[(triple5)] Dave is young.[(triple6 OR ((triple5 ((triple5) -> rule1)) -> rule2))] Gary is furry.[(triple7)] Gary is round.[(triple8)] Gary is white.[(triple9)] Gary is young.[(triple10 OR ((triple9 ((triple9) -> rule1)) -> rule2))] @1: Dave is nice.[(((triple5) -> rule1))] Gary is nice.[(((triple9) -> rule1))] @2: Gary is cold.[(((((triple9) -> rule1) triple10) -> rule3) OR ((((triple9) -> rule1) ((triple9 ((triple9) -> rule1)) -> rule2)) -> rule3))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
((((triple5) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple5 ((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple8
Gary is white.
("Gary" "is" "white" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
((triple9 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple9) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple9) -> (rule1 % int2)) triple10) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple9) -> (rule1 % int3)) ((triple9 ((triple9) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3