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