Charlie is blue. Charlie is quiet. Charlie is young. Smart, quiet things are young. If Charlie is green then Charlie is cold. If Charlie is quiet and Charlie is cold then Charlie is green. If Charlie is young then Charlie is smart. If Charlie is green then Charlie is quiet. All smart things are green.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Smart, quiet things are young.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If Charlie is green then Charlie is cold.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "cold" "+"))
If Charlie is quiet and Charlie is cold then Charlie is green.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "green" "+"))
If Charlie is young then Charlie is smart.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "smart" "+"))
If Charlie is green then Charlie is quiet.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "quiet" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Charlie is young.
True
1
proof
[(triple3)]
("Charlie" "is" "young" "+")
triple3
Charlie is not young.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "young" "-")
triple3
Charlie is smart.
True
2
proof
[(((triple3) -> rule4))]
("Charlie" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple3) -> rule4))]
("Charlie" "is" "smart" "-")
((triple3) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
True
3
proof
[(((((triple3) -> rule4)) -> rule6))]
("Charlie" "is" "green" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("Charlie" "is" "green" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
True
4
proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule2))]
("Charlie" "is" "cold" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not cold.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule2))]
("Charlie" "is" "cold" "-")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
@0: Charlie is blue.[(triple1)] Charlie is quiet.[(triple2 OR ((((((triple3) -> rule4)) -> rule6)) -> rule5))] Charlie is young.[(triple3)] @1: Charlie is smart.[(((triple3) -> rule4))] @2: Charlie is green.[(((((triple3) -> rule4)) -> rule6))] @3: Charlie is cold.[(((((((triple3) -> rule4)) -> rule6)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3