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