Charlie is big. Charlie is rough. Charlie is white. All blue, cold people are smart. If Charlie is blue then Charlie is rough. Blue people are young. If someone is smart and blue then they are cold. If someone is young and big then they are blue. Rough, smart people are big. All rough, big people are young. All white, young people are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
All blue, cold people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is blue then Charlie is rough.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "rough" "+"))
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is smart and blue then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is young and big then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Rough, smart people are big.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All rough, big people are young.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
All white, young people are smart.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Charlie is rough.
True
1
proof
[(triple2)]
("Charlie" "is" "rough" "+")
triple2
Charlie is not white.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "white" "-")
triple3
Charlie is young.
True
3
proof
[(((triple2 triple1) -> rule7))]
("Charlie" "is" "young" "+")
((triple2 triple1) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
3
inv-proof
[(((triple2 triple1) -> rule7))]
("Charlie" "is" "young" "-")
((triple2 triple1) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
True
5
proof
[(((((triple2 triple1) -> rule7) triple1) -> rule5))]
("Charlie" "is" "blue" "+")
((((triple2 triple1) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not smart.
False
5
inv-proof
[(((triple3 ((triple2 triple1) -> rule7)) -> rule8))]
("Charlie" "is" "smart" "-")
((triple3 ((triple2 triple1) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
True
11
proof
[(((((triple3 ((triple2 triple1) -> rule7)) -> rule8) ((((triple2 triple1) -> rule7) triple1) -> rule5)) -> rule4))]
("Charlie" "is" "cold" "+")
((((triple3 ((triple2 triple1) -> (rule7 % int4))) -> (rule8 % int3)) ((((triple2 triple1) -> (rule7 % int4)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is not cold.
False
11
inv-proof
[(((((triple3 ((triple2 triple1) -> rule7)) -> rule8) ((((triple2 triple1) -> rule7) triple1) -> rule5)) -> rule4))]
("Charlie" "is" "cold" "-")
((((triple3 ((triple2 triple1) -> (rule7 % int4))) -> (rule8 % int3)) ((((triple2 triple1) -> (rule7 % int4)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
@0: Charlie is big.[(triple1)] Charlie is rough.[(triple2)] Charlie is white.[(triple3)] @1: Charlie is young.[(((triple2 triple1) -> rule7))] @2: Charlie is blue.[(((((triple2 triple1) -> rule7) triple1) -> rule5))] Charlie is smart.[(((triple3 ((triple2 triple1) -> rule7)) -> rule8))] @3: Charlie is cold.[(((((triple3 ((triple2 triple1) -> rule7)) -> rule8) ((((triple2 triple1) -> rule7) triple1) -> rule5)) -> rule4))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
((triple2 triple1) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2 triple1) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3 ((triple2 triple1) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple3 ((triple2 triple1) -> (rule7 % int4))) -> (rule8 % int3)) ((((triple2 triple1) -> (rule7 % int4)) triple1) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4