Charlie is blue. Charlie is furry. Charlie is nice. Charlie is rough. Charlie is round. Charlie is smart. Erin is blue. Erin is cold. Erin is furry. Erin is rough. If something is round and smart then it is cold. If Erin is blue and Erin is rough then Erin is round. If something is round and cold then it is blue. All nice, smart things are blue. Cold, blue things are round. All round things are smart. All rough things are furry. Rough things are cold.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If something is round and smart then it is cold.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Erin is blue and Erin is rough then Erin is round.
((("Erin" "is" "blue" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "round" "+"))
If something is round and cold then it is blue.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All nice, smart things are blue.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Cold, blue things are round.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Erin is furry.
True
1
proof
[(triple9 OR ((triple10) -> rule7))]
("Erin" "is" "furry" "+")
triple9
((triple10) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Charlie is not rough.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "rough" "-")
triple4
@0: Charlie is blue.[(triple1 OR ((triple3 triple6) -> rule4) OR ((triple3 ((triple5) -> rule6)) -> rule4) OR ((triple5 ((triple4) -> rule8)) -> rule3) OR ((triple5 ((triple5 triple6) -> rule1)) -> rule3) OR ((triple5 ((triple5 ((triple5) -> rule6)) -> rule1)) -> rule3))] Charlie is furry.[(triple2 OR ((triple4) -> rule7))] Charlie is nice.[(triple3)] Charlie is rough.[(triple4)] Charlie is round.[(triple5 OR ((((triple4) -> rule8) triple1) -> rule5) OR ((((triple4) -> rule8) ((triple3 triple6) -> rule4)) -> rule5))] Charlie is smart.[(triple6 OR ((triple5) -> rule6) OR ((((((triple4) -> rule8) triple1) -> rule5)) -> rule6))] Erin is blue.[(triple7)] Erin is cold.[(triple8 OR ((triple10) -> rule8) OR ((((triple7 triple10) -> rule2) ((((triple7 triple10) -> rule2)) -> rule6)) -> rule1))] Erin is furry.[(triple9 OR ((triple10) -> rule7))] Erin is rough.[(triple10)] @1: Charlie is cold.[(((triple4) -> rule8) OR ((triple5 triple6) -> rule1) OR ((triple5 ((triple5) -> rule6)) -> rule1))] Erin is round.[(((triple7 triple10) -> rule2) OR ((triple8 triple7) -> rule5) OR ((((triple10) -> rule8) triple7) -> rule5))] @2: Erin is smart.[(((((triple7 triple10) -> rule2)) -> rule6) OR ((((triple8 triple7) -> rule5)) -> rule6) OR ((((((triple10) -> rule8) triple7) -> rule5)) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple3 triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple3 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((triple5 ((triple4) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((triple5 ((triple5 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((triple5 ((triple5 ((triple5) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple4) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
((((triple4) -> (rule8 % int2)) triple1) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple4) -> (rule8 % int3)) ((triple3 triple6) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple5) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((((triple4) -> (rule8 % int3)) triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple10) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple7 triple10) -> (rule2 % int3)) ((((triple7 triple10) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple10) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple4) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple5 triple6) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple5 ((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple7 triple10) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple8 triple7) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple10) -> (rule8 % int2)) triple7) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple7 triple10) -> (rule2 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple8 triple7) -> (rule5 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple10) -> (rule8 % int3)) triple7) -> (rule5 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3