Bob is blue. Bob is cold. Bob is rough. Bob is round. Bob is young. Gary is white. Gary is young. If Gary is blue then Gary is cold. If something is rough and smart then it is round. Rough, young things are cold. White, cold things are rough. Rough, young things are smart. All white things are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is blue then Gary is cold.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "cold" "+"))
If something is rough and smart then it is round.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Rough, young things are cold.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
White, cold things are rough.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Rough, young things are smart.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All white things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Bob is young.
True
1
proof
[(triple5)]
("Bob" "is" "young" "+")
triple5
Gary is not white.
False
1
inv-proof
[(triple6)]
("Gary" "is" "white" "-")
triple6
Bob is smart.
True
3
proof
[(((triple3 triple5) -> rule5))]
("Bob" "is" "smart" "+")
((triple3 triple5) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple6) -> rule6))]
("Gary" "is" "blue" "-")
((triple6) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
True
3
proof
[(((((triple6) -> rule6)) -> rule1))]
("Gary" "is" "cold" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not cold.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule1))]
("Gary" "is" "cold" "-")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is rough.
True
5
proof
[(((triple6 ((((triple6) -> rule6)) -> rule1)) -> rule4))]
("Gary" "is" "rough" "+")
((triple6 ((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not rough.
False
5
inv-proof
[(((triple6 ((((triple6) -> rule6)) -> rule1)) -> rule4))]
("Gary" "is" "rough" "-")
((triple6 ((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple3 triple5) -> rule3))] Bob is rough.[(triple3)] Bob is round.[(triple4 OR ((triple3 ((triple3 triple5) -> rule5)) -> rule2))] Bob is young.[(triple5)] Gary is white.[(triple6)] Gary is young.[(triple7)] @1: Bob is smart.[(((triple3 triple5) -> rule5))] Gary is blue.[(((triple6) -> rule6))] @2: Gary is cold.[(((((triple6) -> rule6)) -> rule1))] @3: Gary is rough.[(((triple6 ((((triple6) -> rule6)) -> rule1)) -> rule4))] @4: Gary is smart.[(((((triple6 ((((triple6) -> rule6)) -> rule1)) -> rule4) triple7) -> rule5))] @5: Gary is round.[(((((triple6 ((((triple6) -> rule6)) -> rule1)) -> rule4) ((((triple6 ((((triple6) -> rule6)) -> rule1)) -> rule4) triple7) -> rule5)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple3 triple5) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple3 ((triple3 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
((triple3 triple5) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple6) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple6 ((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((triple6 ((((triple6) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple7) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
((((triple6 ((((triple6) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule4 % int3)) ((((triple6 ((((triple6) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule4 % int3)) triple7) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5