Bob is big. Bob is blue. Bob is young. If Bob is white then Bob is quiet. Blue things are quiet. If something is blue then it is quiet. Green things are white. Blue things are green. If Bob is blue then Bob is not round. If something is blue and not quiet then it is not young. If something is blue and not quiet then it is not young.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is young.
("Bob" "is" "young" "+")
If Bob is white then Bob is quiet.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "quiet" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Bob is blue then Bob is not round.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "round" "-"))
If something is blue and not quiet then it is not young.
((("something" "is" "blue" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "-"))
If something is blue and not quiet then it is not young.
((("something" "is" "blue" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "-"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not young.
False
1
inv-proof
[(triple3)]
("Bob" "is" "young" "-")
triple3
Bob is quiet.
True
2
proof
[(((triple2) -> rule2) OR ((triple2) -> rule3) OR ((((((triple2) -> rule5)) -> rule4)) -> rule1))]
("Bob" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is round.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "round" "+")
((triple2) -> (rule6 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is white.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("Bob" "is" "white" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule4))]
("Bob" "is" "white" "-")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is young.[(triple3)] @1: Bob is green.[(((triple2) -> rule5))] Bob is not round.[(((triple2) -> rule6))] Bob is quiet.[(((triple2) -> rule2) OR ((triple2) -> rule3) OR ((((((triple2) -> rule5)) -> rule4)) -> rule1))] @2: Bob is white.[(((((triple2) -> rule5)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not round.
("Bob" "is" "round" "-")
((triple2) -> (rule6 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2