Charlie is big. Charlie is blue. Charlie is nice. Charlie is rough. Charlie is round. Charlie is smart. Charlie is white. Erin is big. Erin is nice. Erin is rough. Erin is round. Erin is smart. If someone is white and not big then they are smart. If someone is rough and not nice then they are not smart. All round people are blue. If someone is round and white then they are blue. If someone is blue then they are white. If Charlie is big and Charlie is round then Charlie is white.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If someone is white and not big then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "smart" "+"))
If someone is rough and not nice then they are not smart.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "smart" "-"))
All round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is round and white then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Charlie is big and Charlie is round then Charlie is white.
((("Charlie" "is" "big" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "white" "+"))
Erin is big.
True
1
proof
[(triple8)]
("Erin" "is" "big" "+")
triple8
Charlie is not smart.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "smart" "-")
triple6
Erin is blue.
True
2
proof
[(((triple11) -> rule3))]
("Erin" "is" "blue" "+")
((triple11) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple11) -> rule3))]
("Erin" "is" "blue" "-")
((triple11) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2 OR ((triple5) -> rule3) OR ((triple5 triple7) -> rule4) OR ((triple5 ((triple1 triple5) -> rule6)) -> rule4))] Charlie is nice.[(triple3)] Charlie is rough.[(triple4)] Charlie is round.[(triple5)] Charlie is smart.[(triple6)] Charlie is white.[(triple7 OR ((triple2) -> rule5) OR ((triple1 triple5) -> rule6) OR ((((triple5) -> rule3)) -> rule5))] Erin is big.[(triple8)] Erin is nice.[(triple9)] Erin is rough.[(triple10)] Erin is round.[(triple11)] Erin is smart.[(triple12)] @1: Erin is blue.[(((triple11) -> rule3))] @2: Erin is white.[(((((triple11) -> rule3)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
((triple5) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple5 triple7) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple5 ((triple1 triple5) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple2) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple1 triple5) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Erin is blue.
("Erin" "is" "blue" "+")
((triple11) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple11) -> (rule3 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2