Charlie is blue. Charlie is green. Charlie is rough. Rough people are round. Quiet people are round. If Charlie is white and Charlie is blue then Charlie is green. All nice, green people are round. White, rough people are quiet. Quiet, round people are white. All blue, rough people are quiet. If Charlie is nice and Charlie is green then Charlie is quiet.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Charlie is white and Charlie is blue then Charlie is green.
((("Charlie" "is" "white" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "green" "+"))
All nice, green people are round.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
White, rough people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Quiet, round people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All blue, rough people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is nice and Charlie is green then Charlie is quiet.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "quiet" "+"))
Charlie is rough.
True
1
proof
[(triple3)]
("Charlie" "is" "rough" "+")
triple3
Charlie is not green.
False
1
inv-proof
[(triple2 OR ((((((triple1 triple3) -> rule7) ((triple3) -> rule1)) -> rule6) triple1) -> rule3) OR ((((((triple1 triple3) -> rule7) ((((triple1 triple3) -> rule7)) -> rule2)) -> rule6) triple1) -> rule3))]
("Charlie" "is" "green" "-")
triple2
((((((triple1 triple3) -> (rule7 % int4)) ((triple3) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple1 triple3) -> (rule7 % int4)) ((((triple1 triple3) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is quiet.
True
3
proof
[(((triple1 triple3) -> rule7))]
("Charlie" "is" "quiet" "+")
((triple1 triple3) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((triple1 triple3) -> rule7)) -> rule2))]
("Charlie" "is" "round" "-")
((triple3) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple1 triple3) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
True
6
proof
[(((((triple1 triple3) -> rule7) ((triple3) -> rule1)) -> rule6) OR ((((triple1 triple3) -> rule7) ((((triple1 triple3) -> rule7)) -> rule2)) -> rule6))]
("Charlie" "is" "white" "+")
((((triple1 triple3) -> (rule7 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple1 triple3) -> (rule7 % int3)) ((((triple1 triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not white.
False
6
inv-proof
[(((((triple1 triple3) -> rule7) ((triple3) -> rule1)) -> rule6) OR ((((triple1 triple3) -> rule7) ((((triple1 triple3) -> rule7)) -> rule2)) -> rule6))]
("Charlie" "is" "white" "-")
((((triple1 triple3) -> (rule7 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple1 triple3) -> (rule7 % int3)) ((((triple1 triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
@0: Charlie is blue.[(triple1)] Charlie is green.[(triple2 OR ((((((triple1 triple3) -> rule7) ((triple3) -> rule1)) -> rule6) triple1) -> rule3) OR ((((((triple1 triple3) -> rule7) ((((triple1 triple3) -> rule7)) -> rule2)) -> rule6) triple1) -> rule3))] Charlie is rough.[(triple3)] @1: Charlie is quiet.[(((triple1 triple3) -> rule7))] Charlie is round.[(((triple3) -> rule1) OR ((((triple1 triple3) -> rule7)) -> rule2))] @2: Charlie is white.[(((((triple1 triple3) -> rule7) ((triple3) -> rule1)) -> rule6) OR ((((triple1 triple3) -> rule7) ((((triple1 triple3) -> rule7)) -> rule2)) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((((((triple1 triple3) -> (rule7 % int4)) ((triple3) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple1 triple3) -> (rule7 % int4)) ((((triple1 triple3) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1 triple3) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple3) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple1 triple3) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1 triple3) -> (rule7 % int3)) ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple1 triple3) -> (rule7 % int3)) ((((triple1 triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3