Dave is green. Dave is nice. Dave is red. Dave is rough. Dave is round. Harry is big. Harry is nice. Harry is not red. Harry is rough. Harry is round. If something is nice then it is green. If something is smart and not rough then it is green. Smart things are not green. Nice things are green. If something is nice and not red then it is green. Green things are not smart.
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is smart and not rough then it is green.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "green" "+"))
Smart things are not green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "-"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is nice and not red then it is green.
((("something" "is" "nice" "+") ("something" "is" "red" "~")) -> ("something" "is" "green" "+"))
Green things are not smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "-"))
Dave is green.
True
1
proof
[(triple1 OR ((triple2) -> rule1) OR ((triple2) -> rule4))]
("Dave" "is" "green" "+")
triple1
((triple2) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not round.
False
1
inv-proof
[(triple5)]
("Dave" "is" "round" "-")
triple5
Harry is green.
True
2
proof
[(((triple7) -> rule1) OR ((triple7) -> rule4) OR ((triple7 triple8) -> rule5))]
("Harry" "is" "green" "+")
((triple7) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple7) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple7 triple8) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple7) -> rule1) OR ((triple7) -> rule4) OR ((triple7 triple8) -> rule5))]
("Harry" "is" "green" "-")
((triple7) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple7) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple7 triple8) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not smart.
True
3
proof
[(((((triple7) -> rule1)) -> rule6) OR ((((triple7) -> rule4)) -> rule6) OR ((((triple7 triple8) -> rule5)) -> rule6))]
("Harry" "is" "smart" "-")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple8) -> (rule5 % int2))) -> (rule6 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule6) OR ((((triple7) -> rule4)) -> rule6) OR ((((triple7 triple8) -> rule5)) -> rule6))]
("Harry" "is" "smart" "+")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple8) -> (rule5 % int2))) -> (rule6 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
@0: Dave is green.[(triple1 OR ((triple2) -> rule1) OR ((triple2) -> rule4))] Dave is nice.[(triple2)] Dave is red.[(triple3)] Dave is rough.[(triple4)] Dave is round.[(triple5)] Harry is big.[(triple6)] Harry is nice.[(triple7)] Harry is not red.[(triple8)] Harry is rough.[(triple9)] Harry is round.[(triple10)] @1: Dave is not smart.[(((triple1) -> rule6) OR ((((triple2) -> rule1)) -> rule6) OR ((((triple2) -> rule4)) -> rule6))] Harry is green.[(((triple7) -> rule1) OR ((triple7) -> rule4) OR ((triple7 triple8) -> rule5))] @2: Harry is not smart.[(((((triple7) -> rule1)) -> rule6) OR ((((triple7) -> rule4)) -> rule6) OR ((((triple7 triple8) -> rule5)) -> rule6))]
Dave is green.
("Dave" "is" "green" "+")
triple1
((triple2) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple2) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Harry is not red.
("Harry" "is" "red" "-")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Dave is not smart.
("Dave" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple7) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple7) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple7 triple8) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple8) -> (rule5 % int2))) -> (rule6 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2