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