Dave is big. Dave is rough. Dave is young. If someone is furry then they are rough. If someone is blue then they are cold. Blue people are red. Young, cold people are blue. If someone is blue then they are furry. If Dave is furry then Dave is cold. If someone is young then they are cold. If someone is cold then they are blue.
Dave is big.
("Dave" "is" "big" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue then they are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Young, cold people are blue.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Dave is furry then Dave is cold.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "cold" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not young.
False
1
inv-proof
[(triple3)]
("Dave" "is" "young" "-")
triple3
Dave is cold.
True
2
proof
[(((triple3) -> rule7))]
("Dave" "is" "cold" "+")
((triple3) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple3) -> rule7))]
("Dave" "is" "cold" "-")
((triple3) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
True
3
proof
[(((((triple3) -> rule7)) -> rule8) OR ((triple3 ((triple3) -> rule7)) -> rule4))]
("Dave" "is" "blue" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple3 ((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule8) OR ((triple3 ((triple3) -> rule7)) -> rule4))]
("Dave" "is" "blue" "-")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple3 ((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
@0: Dave is big.[(triple1)] Dave is rough.[(triple2 OR ((((((((triple3) -> rule7)) -> rule8)) -> rule5)) -> rule1) OR ((((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule5)) -> rule1))] Dave is young.[(triple3)] @1: Dave is cold.[(((triple3) -> rule7))] @2: Dave is blue.[(((((triple3) -> rule7)) -> rule8) OR ((triple3 ((triple3) -> rule7)) -> rule4))] @3: Dave is furry.[(((((((triple3) -> rule7)) -> rule8)) -> rule5) OR ((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule5))] Dave is red.[(((((((triple3) -> rule7)) -> rule8)) -> rule3) OR ((((triple3 ((triple3) -> rule7)) -> rule4)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
((((((((triple3) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((((triple3 ((triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple3) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((triple3 ((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((triple3 ((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((triple3 ((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3