Bob is not big. Bob is not blue. Bob is nice. Bob is red. Bob is round. Bob is smart. Bob is white. Erin is not big. Erin is blue. Erin is round. All blue things are smart. White, big things are red. If Bob is big then Bob is not white. If something is big and red then it is not white. All round things are white. If Erin is round and Erin is white then Erin is red. If Erin is not big then Erin is round. If something is blue then it is nice.
Bob is not big.
("Bob" "is" "big" "-")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is round.
("Erin" "is" "round" "+")
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
White, big things are red.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If Bob is big then Bob is not white.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "white" "-"))
If something is big and red then it is not white.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "-"))
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Erin is round and Erin is white then Erin is red.
((("Erin" "is" "round" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "red" "+"))
If Erin is not big then Erin is round.
((("Erin" "is" "big" "~")) -> ("Erin" "is" "round" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Bob is not blue.
True
1
proof
[(triple2)]
("Bob" "is" "blue" "-")
triple2
Bob is not round.
False
1
inv-proof
[(triple5)]
("Bob" "is" "round" "-")
triple5
Erin is nice.
True
2
proof
[(((triple9) -> rule8))]
("Erin" "is" "nice" "+")
((triple9) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple9) -> rule8))]
("Erin" "is" "nice" "-")
((triple9) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
True
4
proof
[(((triple10 ((triple10) -> rule5)) -> rule6) OR ((((triple8) -> rule7) ((triple10) -> rule5)) -> rule6) OR ((triple10 ((((triple8) -> rule7)) -> rule5)) -> rule6) OR ((((triple8) -> rule7) ((((triple8) -> rule7)) -> rule5)) -> rule6))]
("Erin" "is" "red" "+")
((triple10 ((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple8) -> (rule7 % int3)) ((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((triple10 ((((triple8) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple8) -> (rule7 % int3)) ((((triple8) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not red.
False
4
inv-proof
[(((triple10 ((triple10) -> rule5)) -> rule6) OR ((((triple8) -> rule7) ((triple10) -> rule5)) -> rule6) OR ((triple10 ((((triple8) -> rule7)) -> rule5)) -> rule6) OR ((((triple8) -> rule7) ((((triple8) -> rule7)) -> rule5)) -> rule6))]
("Erin" "is" "red" "-")
((triple10 ((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple8) -> (rule7 % int3)) ((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((triple10 ((((triple8) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple8) -> (rule7 % int3)) ((((triple8) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
@0: Bob is nice.[(triple3)] Bob is not big.[(triple1)] Bob is not blue.[(triple2)] Bob is red.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7 OR ((triple5) -> rule5))] Erin is blue.[(triple9)] Erin is not big.[(triple8)] Erin is round.[(triple10 OR ((triple8) -> rule7))] @1: Erin is nice.[(((triple9) -> rule8))] Erin is smart.[(((triple9) -> rule1))] Erin is white.[(((triple10) -> rule5) OR ((((triple8) -> rule7)) -> rule5))] @2: Erin is red.[(((triple10 ((triple10) -> rule5)) -> rule6) OR ((((triple8) -> rule7) ((triple10) -> rule5)) -> rule6) OR ((triple10 ((((triple8) -> rule7)) -> rule5)) -> rule6) OR ((((triple8) -> rule7) ((((triple8) -> rule7)) -> rule5)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not blue.
("Bob" "is" "blue" "-")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple5) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple9
Erin is not big.
("Erin" "is" "big" "-")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple10
((triple8) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple9) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple9) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple10) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple8) -> (rule7 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple10 ((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple8) -> (rule7 % int3)) ((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((triple10 ((((triple8) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple8) -> (rule7 % int3)) ((((triple8) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3