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