Bob is red. Bob is round. Bob is white. If Bob is smart and Bob is round then Bob is white. Round things are white. If Bob is red and Bob is smart then Bob is young. If something is blue then it is quiet. All smart, round things are blue. If Bob is white then Bob is smart.
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
If Bob is smart and Bob is round then Bob is white.
((("Bob" "is" "smart" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "white" "+"))
Round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Bob is red and Bob is smart then Bob is young.
((("Bob" "is" "red" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "young" "+"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
All smart, round things are blue.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If Bob is white then Bob is smart.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "smart" "+"))
Bob is round.
True
1
proof
[(triple2)]
("Bob" "is" "round" "+")
triple2
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Bob is smart.
True
2
proof
[(((triple3) -> rule6) OR ((((triple2) -> rule2)) -> rule6))]
("Bob" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not smart.
False
2
inv-proof
[(((triple3) -> rule6) OR ((((triple2) -> rule2)) -> rule6))]
("Bob" "is" "smart" "-")
((triple3) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
True
4
proof
[(((((triple3) -> rule6) triple2) -> rule5) OR ((((((triple2) -> rule2)) -> rule6) triple2) -> rule5))]
("Bob" "is" "blue" "+")
((((triple3) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not young.
False
4
inv-proof
[(((triple1 ((triple3) -> rule6)) -> rule3) OR ((triple1 ((((triple2) -> rule2)) -> rule6)) -> rule3))]
("Bob" "is" "young" "-")
((triple1 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((triple1 ((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is quiet.
True
5
proof
[(((((((triple3) -> rule6) triple2) -> rule5)) -> rule4) OR ((((((((triple2) -> rule2)) -> rule6) triple2) -> rule5)) -> rule4))]
("Bob" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((((triple2) -> (rule2 % int4))) -> (rule6 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not quiet.
False
5
inv-proof
[(((((((triple3) -> rule6) triple2) -> rule5)) -> rule4) OR ((((((((triple2) -> rule2)) -> rule6) triple2) -> rule5)) -> rule4))]
("Bob" "is" "quiet" "-")
((((((triple3) -> (rule6 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((((triple2) -> (rule2 % int4))) -> (rule6 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
@0: Bob is red.[(triple1)] Bob is round.[(triple2)] Bob is white.[(triple3 OR ((triple2) -> rule2))] @1: Bob is smart.[(((triple3) -> rule6) OR ((((triple2) -> rule2)) -> rule6))] @2: Bob is blue.[(((((triple3) -> rule6) triple2) -> rule5) OR ((((((triple2) -> rule2)) -> rule6) triple2) -> rule5))] Bob is young.[(((triple1 ((triple3) -> rule6)) -> rule3) OR ((triple1 ((((triple2) -> rule2)) -> rule6)) -> rule3))] @3: Bob is quiet.[(((((((triple3) -> rule6) triple2) -> rule5)) -> rule4) OR ((((((((triple2) -> rule2)) -> rule6) triple2) -> rule5)) -> rule4))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
((triple2) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((triple3) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((triple1 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((triple1 ((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((((triple2) -> (rule2 % int4))) -> (rule6 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4