Erin is big. Erin is blue. Erin is nice. Erin is quiet. Erin is round. Erin is smart. Erin is white. Fiona is big. Fiona is blue. Fiona is nice. Fiona is quiet. Fiona is round. Fiona is smart. Fiona is white. Big things are round. If something is smart and not nice then it is not round. If something is nice and smart then it is big. If Fiona is nice and Fiona is not blue then Fiona is smart. If Fiona is quiet then Fiona is round. If something is blue and not big then it is not quiet.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is smart and not nice then it is not round.
((("something" "is" "smart" "+") ("something" "is" "nice" "~")) -> ("something" "is" "round" "-"))
If something is nice and smart then it is big.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If Fiona is nice and Fiona is not blue then Fiona is smart.
((("Fiona" "is" "nice" "+") ("Fiona" "is" "blue" "~")) -> ("Fiona" "is" "smart" "+"))
If Fiona is quiet then Fiona is round.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "round" "+"))
If something is blue and not big then it is not quiet.
((("something" "is" "blue" "+") ("something" "is" "big" "~")) -> ("something" "is" "quiet" "-"))
Fiona is smart.
True
1
proof
[(triple13)]
("Fiona" "is" "smart" "+")
triple13
Fiona is not round.
False
1
inv-proof
[(triple12 OR ((triple11) -> rule5) OR ((triple8) -> rule1) OR ((((triple10 triple13) -> rule3)) -> rule1))]
("Fiona" "is" "round" "-")
triple12
((triple11) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple8) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple10 triple13) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
@0: Erin is big.[(triple1 OR ((triple3 triple6) -> rule3))] Erin is blue.[(triple2)] Erin is nice.[(triple3)] Erin is quiet.[(triple4)] Erin is round.[(triple5 OR ((triple1) -> rule1) OR ((((triple3 triple6) -> rule3)) -> rule1))] Erin is smart.[(triple6)] Erin is white.[(triple7)] Fiona is big.[(triple8 OR ((triple10 triple13) -> rule3))] Fiona is blue.[(triple9)] Fiona is nice.[(triple10)] Fiona is quiet.[(triple11)] Fiona is round.[(triple12 OR ((triple11) -> rule5) OR ((triple8) -> rule1) OR ((((triple10 triple13) -> rule3)) -> rule1))] Fiona is smart.[(triple13)] Fiona is white.[(triple14)]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple3 triple6) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple1) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple3 triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
((triple10 triple13) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is round.
("Fiona" "is" "round" "+")
triple12
((triple11) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple8) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple10 triple13) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple13
Fiona is white.
("Fiona" "is" "white" "+")
triple14