Charlie is blue. Charlie is quiet. Charlie is round. If something is quiet and green then it is white. If something is green and white then it is blue. If something is green then it is white. If Charlie is white then Charlie is nice. If Charlie is cold then Charlie is quiet. All round, blue things are green.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
If something is quiet and green then it is white.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is green and white then it is blue.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If Charlie is white then Charlie is nice.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "nice" "+"))
If Charlie is cold then Charlie is quiet.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "quiet" "+"))
All round, blue things are green.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Charlie is not quiet.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Charlie is green.
True
3
proof
[(((triple3 triple1) -> rule6))]
("Charlie" "is" "green" "+")
((triple3 triple1) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
3
inv-proof
[(((triple3 triple1) -> rule6))]
("Charlie" "is" "green" "-")
((triple3 triple1) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
True
4
proof
[(((((triple3 triple1) -> rule6)) -> rule3) OR ((triple2 ((triple3 triple1) -> rule6)) -> rule1))]
("Charlie" "is" "white" "+")
((((triple3 triple1) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple2 ((triple3 triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((((triple3 triple1) -> rule6)) -> rule3) OR ((triple2 ((triple3 triple1) -> rule6)) -> rule1))]
("Charlie" "is" "white" "-")
((((triple3 triple1) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple2 ((triple3 triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
True
5
proof
[(((((((triple3 triple1) -> rule6)) -> rule3)) -> rule4) OR ((((triple2 ((triple3 triple1) -> rule6)) -> rule1)) -> rule4))]
("Charlie" "is" "nice" "+")
((((((triple3 triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple2 ((triple3 triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not nice.
False
5
inv-proof
[(((((((triple3 triple1) -> rule6)) -> rule3)) -> rule4) OR ((((triple2 ((triple3 triple1) -> rule6)) -> rule1)) -> rule4))]
("Charlie" "is" "nice" "-")
((((((triple3 triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple2 ((triple3 triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
@0: Charlie is blue.[(triple1)] Charlie is quiet.[(triple2)] Charlie is round.[(triple3)] @1: Charlie is green.[(((triple3 triple1) -> rule6))] @2: Charlie is white.[(((((triple3 triple1) -> rule6)) -> rule3) OR ((triple2 ((triple3 triple1) -> rule6)) -> rule1))] @3: Charlie is nice.[(((((((triple3 triple1) -> rule6)) -> rule3)) -> rule4) OR ((((triple2 ((triple3 triple1) -> rule6)) -> rule1)) -> rule4))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple3 triple1) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple3 triple1) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple2 ((triple3 triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple3 triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple2 ((triple3 triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3