Gary is cold. Gary is nice. Gary is quiet. Gary is rough. Gary is round. Gary is smart. Gary is white. Harry is rough. Harry is not smart. Harry is white. Round things are quiet. White things are quiet. If something is quiet and not smart then it is white. If something is cold and not rough then it is white. If Harry is white then Harry is cold. If something is rough then it is round.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is white.
("Harry" "is" "white" "+")
Round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
White things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and not smart then it is white.
((("something" "is" "quiet" "+") ("something" "is" "smart" "~")) -> ("something" "is" "white" "+"))
If something is cold and not rough then it is white.
((("something" "is" "cold" "+") ("something" "is" "rough" "~")) -> ("something" "is" "white" "+"))
If Harry is white then Harry is cold.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "cold" "+"))
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Harry is rough.
True
1
proof
[(triple8)]
("Harry" "is" "rough" "+")
triple8
Gary is not nice.
False
1
inv-proof
[(triple2)]
("Gary" "is" "nice" "-")
triple2
@0: Gary is cold.[(triple1)] Gary is nice.[(triple2)] Gary is quiet.[(triple3 OR ((triple5) -> rule1) OR ((triple7) -> rule2) OR ((((triple4) -> rule6)) -> rule1))] Gary is rough.[(triple4)] Gary is round.[(triple5 OR ((triple4) -> rule6))] Gary is smart.[(triple6)] Gary is white.[(triple7)] Harry is not smart.[(triple9)] Harry is rough.[(triple8)] Harry is white.[(triple10 OR ((((((triple8) -> rule6)) -> rule1) triple9) -> rule3))] @1: Harry is cold.[(((triple10) -> rule5) OR ((((((((triple8) -> rule6)) -> rule1) triple9) -> rule3)) -> rule5))] Harry is quiet.[(((triple10) -> rule2) OR ((((triple8) -> rule6)) -> rule1))] Harry is round.[(((triple8) -> rule6))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
((triple5) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple7) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
((triple4) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Harry is not smart.
("Harry" "is" "smart" "-")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is white.
("Harry" "is" "white" "+")
triple10
((((((triple8) -> (rule6 % int3))) -> (rule1 % int2)) triple9) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((triple10) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((((((triple8) -> (rule6 % int4))) -> (rule1 % int3)) triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple10) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple8) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1