Gary is cold. Gary is green. Gary is kind. Gary is quiet. Gary is red. Gary is round. Harry is cold. Harry is green. Harry is kind. Harry is quiet. Harry is red. Harry is smart. If Gary is kind then Gary is smart. All quiet people are green. Cold, smart people are quiet.
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Gary is kind then Gary is smart.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "smart" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Cold, smart people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Harry is not quiet.
False
1
inv-proof
[(triple10 OR ((triple7 triple12) -> rule3))]
("Harry" "is" "quiet" "-")
triple10
((triple7 triple12) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Gary is smart.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
@0: Gary is cold.[(triple1)] Gary is green.[(triple2 OR ((triple4) -> rule2) OR ((((triple1 ((triple3) -> rule1)) -> rule3)) -> rule2))] Gary is kind.[(triple3)] Gary is quiet.[(triple4 OR ((triple1 ((triple3) -> rule1)) -> rule3))] Gary is red.[(triple5)] Gary is round.[(triple6)] Harry is cold.[(triple7)] Harry is green.[(triple8 OR ((triple10) -> rule2) OR ((((triple7 triple12) -> rule3)) -> rule2))] Harry is kind.[(triple9)] Harry is quiet.[(triple10 OR ((triple7 triple12) -> rule3))] Harry is red.[(triple11)] Harry is smart.[(triple12)] @1: Gary is smart.[(((triple3) -> rule1))]
Gary is cold.
("Gary" "is" "cold" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
((triple4) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple1 ((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
((triple1 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
((triple10) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple7 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple7 triple12) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1