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