Anne is blue. Anne is cold. Anne is green. Anne is quiet. Anne is red. Anne is rough. Anne is smart. Harry is blue. Harry is cold. Harry is quiet. Harry is red. Harry is smart. If someone is green then they are smart. If someone is cold and quiet then they are green. If someone is green and blue then they are quiet. Blue, quiet people are rough. Rough, cold people are smart. Red, cold people are smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is green then they are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold and quiet then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is green and blue then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Blue, quiet people are rough.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Rough, cold people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Red, cold people are smart.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Anne is red.
True
1
proof
[(triple5)]
("Anne" "is" "red" "+")
triple5
Harry is not smart.
False
1
inv-proof
[(triple12 OR ((triple11 triple9) -> rule6) OR ((((triple9 triple10) -> rule2)) -> rule1) OR ((((triple8 triple10) -> rule4) triple9) -> rule5))]
("Harry" "is" "smart" "-")
triple12
((triple11 triple9) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple9 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple8 triple10) -> (rule4 % int2)) triple9) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is rough.
True
3
proof
[(((triple8 triple10) -> rule4))]
("Harry" "is" "rough" "+")
((triple8 triple10) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not green.
False
3
inv-proof
[(((triple9 triple10) -> rule2))]
("Harry" "is" "green" "-")
((triple9 triple10) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is green.[(triple3 OR ((triple2 triple4) -> rule2))] Anne is quiet.[(triple4 OR ((triple3 triple1) -> rule3))] Anne is red.[(triple5)] Anne is rough.[(triple6 OR ((triple1 triple4) -> rule4) OR ((triple1 ((triple3 triple1) -> rule3)) -> rule4))] Anne is smart.[(triple7 OR ((triple3) -> rule1) OR ((triple5 triple2) -> rule6) OR ((triple6 triple2) -> rule5) OR ((((triple2 triple4) -> rule2)) -> rule1) OR ((((triple1 triple4) -> rule4) triple2) -> rule5) OR ((((triple1 ((triple3 triple1) -> rule3)) -> rule4) triple2) -> rule5))] Harry is blue.[(triple8)] Harry is cold.[(triple9)] Harry is quiet.[(triple10)] Harry is red.[(triple11)] Harry is smart.[(triple12 OR ((triple11 triple9) -> rule6) OR ((((triple9 triple10) -> rule2)) -> rule1) OR ((((triple8 triple10) -> rule4) triple9) -> rule5))] @1: Harry is green.[(((triple9 triple10) -> rule2))] Harry is rough.[(((triple8 triple10) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple2 triple4) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple3 triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
((triple1 triple4) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple1 ((triple3 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple7
((triple3) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple5 triple2) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple6 triple2) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2 triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple1 triple4) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple1 ((triple3 triple1) -> (rule3 % int3))) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple11 triple9) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple9 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple8 triple10) -> (rule4 % int2)) triple9) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple9 triple10) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple8 triple10) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1