Charlie is cold. Charlie is kind. Charlie is nice. Cold people are kind. If someone is young then they are cold. Young, nice people are cold. If Charlie is green and Charlie is rough then Charlie is white. If Charlie is nice and Charlie is rough then Charlie is white. Kind, green people are rough. If Charlie is green and Charlie is nice then Charlie is rough. If someone is nice then they are green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Young, nice people are cold.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is green and Charlie is rough then Charlie is white.
((("Charlie" "is" "green" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "white" "+"))
If Charlie is nice and Charlie is rough then Charlie is white.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "white" "+"))
Kind, green people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is green and Charlie is nice then Charlie is rough.
((("Charlie" "is" "green" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "rough" "+"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Charlie is kind.
True
1
proof
[(triple2 OR ((triple1) -> rule1))]
("Charlie" "is" "kind" "+")
triple2
((triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "-")
triple3
Charlie is green.
True
2
proof
[(((triple3) -> rule8))]
("Charlie" "is" "green" "+")
((triple3) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple3) -> rule8))]
("Charlie" "is" "green" "-")
((triple3) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
True
4
proof
[(((triple2 ((triple3) -> rule8)) -> rule6) OR ((((triple3) -> rule8) triple3) -> rule7) OR ((((triple1) -> rule1) ((triple3) -> rule8)) -> rule6))]
("Charlie" "is" "rough" "+")
((triple2 ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple3) -> (rule8 % int2)) triple3) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not rough.
False
4
inv-proof
[(((triple2 ((triple3) -> rule8)) -> rule6) OR ((((triple3) -> rule8) triple3) -> rule7) OR ((((triple1) -> rule1) ((triple3) -> rule8)) -> rule6))]
("Charlie" "is" "rough" "-")
((triple2 ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple3) -> (rule8 % int2)) triple3) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is white.
True
6
proof
[(((triple3 ((triple2 ((triple3) -> rule8)) -> rule6)) -> rule5) OR ((triple3 ((((triple3) -> rule8) triple3) -> rule7)) -> rule5) OR ((triple3 ((((triple1) -> rule1) ((triple3) -> rule8)) -> rule6)) -> rule5) OR ((((triple3) -> rule8) ((triple2 ((triple3) -> rule8)) -> rule6)) -> rule4) OR ((((triple3) -> rule8) ((((triple3) -> rule8) triple3) -> rule7)) -> rule4) OR ((((triple3) -> rule8) ((((triple1) -> rule1) ((triple3) -> rule8)) -> rule6)) -> rule4))]
("Charlie" "is" "white" "+")
((triple3 ((triple2 ((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((triple3 ((((triple3) -> (rule8 % int3)) triple3) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((triple3 ((((triple1) -> (rule1 % int4)) ((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((triple3) -> (rule8 % int3)) ((triple2 ((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple3) -> (rule8 % int3)) ((((triple3) -> (rule8 % int3)) triple3) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple3) -> (rule8 % int4)) ((((triple1) -> (rule1 % int3)) ((triple3) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is not white.
False
6
inv-proof
[(((triple3 ((triple2 ((triple3) -> rule8)) -> rule6)) -> rule5) OR ((triple3 ((((triple3) -> rule8) triple3) -> rule7)) -> rule5) OR ((triple3 ((((triple1) -> rule1) ((triple3) -> rule8)) -> rule6)) -> rule5) OR ((((triple3) -> rule8) ((triple2 ((triple3) -> rule8)) -> rule6)) -> rule4) OR ((((triple3) -> rule8) ((((triple3) -> rule8) triple3) -> rule7)) -> rule4) OR ((((triple3) -> rule8) ((((triple1) -> rule1) ((triple3) -> rule8)) -> rule6)) -> rule4))]
("Charlie" "is" "white" "-")
((triple3 ((triple2 ((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((triple3 ((((triple3) -> (rule8 % int3)) triple3) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((triple3 ((((triple1) -> (rule1 % int4)) ((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((triple3) -> (rule8 % int3)) ((triple2 ((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple3) -> (rule8 % int3)) ((((triple3) -> (rule8 % int3)) triple3) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple3) -> (rule8 % int4)) ((((triple1) -> (rule1 % int3)) ((triple3) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
@0: Charlie is cold.[(triple1)] Charlie is kind.[(triple2 OR ((triple1) -> rule1))] Charlie is nice.[(triple3)] @1: Charlie is green.[(((triple3) -> rule8))] @2: Charlie is rough.[(((triple2 ((triple3) -> rule8)) -> rule6) OR ((((triple3) -> rule8) triple3) -> rule7) OR ((((triple1) -> rule1) ((triple3) -> rule8)) -> rule6))] @3: Charlie is white.[(((triple3 ((triple2 ((triple3) -> rule8)) -> rule6)) -> rule5) OR ((triple3 ((((triple3) -> rule8) triple3) -> rule7)) -> rule5) OR ((triple3 ((((triple1) -> rule1) ((triple3) -> rule8)) -> rule6)) -> rule5) OR ((((triple3) -> rule8) ((triple2 ((triple3) -> rule8)) -> rule6)) -> rule4) OR ((((triple3) -> rule8) ((((triple3) -> rule8) triple3) -> rule7)) -> rule4) OR ((((triple3) -> rule8) ((((triple1) -> rule1) ((triple3) -> rule8)) -> rule6)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple3) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2 ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple3) -> (rule8 % int2)) triple3) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple3) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((triple3 ((triple2 ((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((triple3 ((((triple3) -> (rule8 % int3)) triple3) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((triple3 ((((triple1) -> (rule1 % int4)) ((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((triple3) -> (rule8 % int3)) ((triple2 ((triple3) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple3) -> (rule8 % int3)) ((((triple3) -> (rule8 % int3)) triple3) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple3) -> (rule8 % int4)) ((((triple1) -> (rule1 % int3)) ((triple3) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4