Bob is not green. Bob is quiet. Bob is round. All quiet people are big. Green people are quiet. All round people are not green. If Bob is red and Bob is green then Bob is white. Round, green people are not red. If someone is white and not green then they are red. If someone is big and not green then they are white. If someone is big then they are white.
Bob is not green.
("Bob" "is" "green" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All round people are not green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "-"))
If Bob is red and Bob is green then Bob is white.
((("Bob" "is" "red" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "white" "+"))
Round, green people are not red.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "-"))
If someone is white and not green then they are red.
((("someone" "is" "white" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "red" "+"))
If someone is big and not green then they are white.
((("someone" "is" "big" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "white" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Bob is quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Bob is not round.
False
1
inv-proof
[(triple3)]
("Bob" "is" "round" "-")
triple3
Bob is big.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "big" "+")
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "big" "-")
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
True
3
proof
[(((((triple2) -> rule1)) -> rule8) OR ((((triple2) -> rule1) triple1) -> rule7) OR ((((triple2) -> rule1) ((triple3) -> rule3)) -> rule7))]
("Bob" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not white.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule8) OR ((((triple2) -> rule1) triple1) -> rule7) OR ((((triple2) -> rule1) ((triple3) -> rule3)) -> rule7))]
("Bob" "is" "white" "-")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is red.
True
5
proof
[(((((((triple2) -> rule1)) -> rule8) triple1) -> rule6) OR ((((((triple2) -> rule1) triple1) -> rule7) triple1) -> rule6) OR ((((((triple2) -> rule1)) -> rule8) ((triple3) -> rule3)) -> rule6) OR ((((((triple2) -> rule1) triple1) -> rule7) ((triple3) -> rule3)) -> rule6) OR ((((((triple2) -> rule1) ((triple3) -> rule3)) -> rule7) triple1) -> rule6) OR ((((((triple2) -> rule1) ((triple3) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule6))]
("Bob" "is" "red" "+")
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple2) -> (rule1 % int3)) triple1) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple2) -> (rule1 % int4))) -> (rule8 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((((triple2) -> (rule1 % int4)) triple1) -> (rule7 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((((triple2) -> (rule1 % int4)) ((triple3) -> (rule3 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((((triple2) -> (rule1 % int4)) ((triple3) -> (rule3 % int3))) -> (rule7 % int2)) ((triple3) -> (rule3 % int3))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is not red.
False
5
inv-proof
[(((((((triple2) -> rule1)) -> rule8) triple1) -> rule6) OR ((((((triple2) -> rule1) triple1) -> rule7) triple1) -> rule6) OR ((((((triple2) -> rule1)) -> rule8) ((triple3) -> rule3)) -> rule6) OR ((((((triple2) -> rule1) triple1) -> rule7) ((triple3) -> rule3)) -> rule6) OR ((((((triple2) -> rule1) ((triple3) -> rule3)) -> rule7) triple1) -> rule6) OR ((((((triple2) -> rule1) ((triple3) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule6))]
("Bob" "is" "red" "-")
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple2) -> (rule1 % int3)) triple1) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple2) -> (rule1 % int4))) -> (rule8 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((((triple2) -> (rule1 % int4)) triple1) -> (rule7 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((((triple2) -> (rule1 % int4)) ((triple3) -> (rule3 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((((triple2) -> (rule1 % int4)) ((triple3) -> (rule3 % int3))) -> (rule7 % int2)) ((triple3) -> (rule3 % int3))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
@0: Bob is not green.[(triple1 OR ((triple3) -> rule3))] Bob is quiet.[(triple2)] Bob is round.[(triple3)] @1: Bob is big.[(((triple2) -> rule1))] @2: Bob is white.[(((((triple2) -> rule1)) -> rule8) OR ((((triple2) -> rule1) triple1) -> rule7) OR ((((triple2) -> rule1) ((triple3) -> rule3)) -> rule7))] @3: Bob is red.[(((((((triple2) -> rule1)) -> rule8) triple1) -> rule6) OR ((((((triple2) -> rule1) triple1) -> rule7) triple1) -> rule6) OR ((((((triple2) -> rule1)) -> rule8) ((triple3) -> rule3)) -> rule6) OR ((((((triple2) -> rule1) triple1) -> rule7) ((triple3) -> rule3)) -> rule6) OR ((((((triple2) -> rule1) ((triple3) -> rule3)) -> rule7) triple1) -> rule6) OR ((((((triple2) -> rule1) ((triple3) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule6))]
Bob is not green.
("Bob" "is" "green" "-")
triple1
((triple3) -> (rule3 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple2) -> (rule1 % int3)) triple1) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple2) -> (rule1 % int4))) -> (rule8 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((((triple2) -> (rule1 % int4)) triple1) -> (rule7 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((((triple2) -> (rule1 % int4)) ((triple3) -> (rule3 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((((triple2) -> (rule1 % int4)) ((triple3) -> (rule3 % int3))) -> (rule7 % int2)) ((triple3) -> (rule3 % int3))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
int3
Bob is big.
("Bob" "is" "big" "+")
int4