Charlie is furry. Charlie is kind. Charlie is nice. Charlie is red. Charlie is young. Dave is furry. Dave is kind. Dave is nice. Dave is red. Dave is rough. Dave is young. Fiona is nice. Fiona is red. Fiona is rough. Fiona is young. All rough, red things are cold. If Charlie is cold then Charlie is young. If something is nice and rough then it is red. If Dave is nice then Dave is young. All young things are kind. If something is nice then it is cold. All kind, red things are young. Young things are furry.
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 young.
("Charlie" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All rough, red things are cold.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Charlie is cold then Charlie is young.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "young" "+"))
If something is nice and rough then it is red.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If Dave is nice then Dave is young.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "young" "+"))
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All kind, red things are young.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Charlie is red.
True
1
proof
[(triple4)]
("Charlie" "is" "red" "+")
triple4
Dave is not young.
False
1
inv-proof
[(triple11 OR ((triple8) -> rule4) OR ((triple7 triple9) -> rule7) OR ((triple7 ((triple8 triple10) -> rule3)) -> rule7))]
("Dave" "is" "young" "-")
triple11
((triple8) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple7 triple9) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple7 ((triple8 triple10) -> (rule3 % int2))) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Charlie is cold.
True
2
proof
[(((triple3) -> rule6))]
("Charlie" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple12) -> rule6) OR ((triple14 triple13) -> rule1) OR ((triple14 ((triple12 triple14) -> rule3)) -> rule1))]
("Fiona" "is" "cold" "-")
((triple12) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple14 triple13) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple14 ((triple12 triple14) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
@0: Charlie is furry.[(triple1 OR ((triple5) -> rule8) OR ((((triple2 triple4) -> rule7)) -> rule8) OR ((((((triple3) -> rule6)) -> rule2)) -> rule8))] Charlie is kind.[(triple2 OR ((triple5) -> rule5) OR ((((((triple3) -> rule6)) -> rule2)) -> rule5))] Charlie is nice.[(triple3)] Charlie is red.[(triple4)] Charlie is young.[(triple5 OR ((triple2 triple4) -> rule7) OR ((((triple3) -> rule6)) -> rule2))] Dave is furry.[(triple6 OR ((triple11) -> rule8) OR ((((triple8) -> rule4)) -> rule8) OR ((((triple7 triple9) -> rule7)) -> rule8) OR ((((triple7 ((triple8 triple10) -> rule3)) -> rule7)) -> rule8))] Dave is kind.[(triple7 OR ((triple11) -> rule5) OR ((((triple8) -> rule4)) -> rule5))] Dave is nice.[(triple8)] Dave is red.[(triple9 OR ((triple8 triple10) -> rule3))] Dave is rough.[(triple10)] Dave is young.[(triple11 OR ((triple8) -> rule4) OR ((triple7 triple9) -> rule7) OR ((triple7 ((triple8 triple10) -> rule3)) -> rule7))] Fiona is nice.[(triple12)] Fiona is red.[(triple13 OR ((triple12 triple14) -> rule3))] Fiona is rough.[(triple14)] Fiona is young.[(triple15)] @1: Charlie is cold.[(((triple3) -> rule6))] Dave is cold.[(((triple8) -> rule6) OR ((triple10 triple9) -> rule1) OR ((triple10 ((triple8 triple10) -> rule3)) -> rule1))] Fiona is cold.[(((triple12) -> rule6) OR ((triple14 triple13) -> rule1) OR ((triple14 ((triple12 triple14) -> rule3)) -> rule1))] Fiona is furry.[(((triple15) -> rule8))] Fiona is kind.[(((triple15) -> rule5))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
((triple5) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple2 triple4) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple5) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((triple2 triple4) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple6
((triple11) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple7 triple9) -> (rule7 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple7 ((triple8 triple10) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple7
((triple11) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple8 triple10) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
((triple8) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple7 triple9) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple7 ((triple8 triple10) -> (rule3 % int2))) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple12
Fiona is red.
("Fiona" "is" "red" "+")
triple13
((triple12 triple14) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple14
Fiona is young.
("Fiona" "is" "young" "+")
triple15
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple8) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple10 triple9) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple10 ((triple8 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple12) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple14 triple13) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple14 ((triple12 triple14) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple15) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple15) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1