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