Dave is cold. Dave is green. Dave is red. Dave is not round. Dave is smart. Dave is not white. Dave is not young. Harry is cold. Harry is green. Harry is red. Harry is not round. Harry is smart. Harry is white. Harry is young. If someone is red then they are cold. All young people are green. If someone is red then they are smart.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not white.
("Dave" "is" "white" "-")
Dave is not young.
("Dave" "is" "young" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Dave is not round.
True
1
proof
[(triple4)]
("Dave" "is" "round" "-")
triple4
Dave is not smart.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule3))]
("Dave" "is" "smart" "-")
triple5
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
@0: Dave is cold.[(triple1 OR ((triple3) -> rule1))] Dave is green.[(triple2)] Dave is not round.[(triple4)] Dave is not white.[(triple6)] Dave is not young.[(triple7)] Dave is red.[(triple3)] Dave is smart.[(triple5 OR ((triple3) -> rule3))] Harry is cold.[(triple8 OR ((triple10) -> rule1))] Harry is green.[(triple9 OR ((triple14) -> rule2))] Harry is not round.[(triple11)] Harry is red.[(triple10)] Harry is smart.[(triple12 OR ((triple10) -> rule3))] Harry is white.[(triple13)] Harry is young.[(triple14)]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
((triple3) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is not round.
("Dave" "is" "round" "-")
triple4
Dave is not white.
("Dave" "is" "white" "-")
triple6
Dave is not young.
("Dave" "is" "young" "-")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple5
((triple3) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
((triple14) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14