Dave is blue. Dave is cold. Dave is furry. Dave is kind. Dave is red. Dave is rough. Dave is young. Red things are rough. If something is cold then it is blue. All red, blue things are kind. If something is rough and blue then it is kind. If something is furry then it is rough. If something is kind then it is red.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All red, blue things are kind.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is rough and blue then it is kind.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Dave is cold.
True
1
proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple7)]
("Dave" "is" "young" "-")
triple7
@0: Dave is blue.[(triple1 OR ((triple2) -> rule2))] Dave is cold.[(triple2)] Dave is furry.[(triple3)] Dave is kind.[(triple4 OR ((triple5 triple1) -> rule3) OR ((triple6 triple1) -> rule4) OR ((triple5 ((triple2) -> rule2)) -> rule3) OR ((triple6 ((triple2) -> rule2)) -> rule4) OR ((((triple3) -> rule5) triple1) -> rule4) OR ((((triple5) -> rule1) triple1) -> rule4) OR ((((triple3) -> rule5) ((triple2) -> rule2)) -> rule4) OR ((((triple5) -> rule1) ((triple2) -> rule2)) -> rule4))] Dave is red.[(triple5 OR ((triple4) -> rule6) OR ((((triple6 triple1) -> rule4)) -> rule6) OR ((((triple6 ((triple2) -> rule2)) -> rule4)) -> rule6) OR ((((((triple3) -> rule5) triple1) -> rule4)) -> rule6) OR ((((((triple3) -> rule5) ((triple2) -> rule2)) -> rule4)) -> rule6))] Dave is rough.[(triple6 OR ((triple3) -> rule5) OR ((triple5) -> rule1) OR ((((triple4) -> rule6)) -> rule1))] Dave is young.[(triple7)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
((triple5 triple1) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple6 triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple5 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((triple6 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple3) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple5) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple3) -> (rule5 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((triple5) -> (rule1 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple4) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple6 triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple6 ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((triple3) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple3) -> (rule5 % int4)) ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
triple6
((triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple5) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple7