Dave is cold. Dave is green. Dave is rough. If Dave is not cold then Dave is round. All rough, cold people are green. If Dave is cold then Dave is not nice. If someone is cold then they are rough. If someone is rough and not nice then they are round. If someone is round and not cold then they are not big. All green, round people are kind. If someone is green and not big then they are kind.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
If Dave is not cold then Dave is round.
((("Dave" "is" "cold" "~")) -> ("Dave" "is" "round" "+"))
All rough, cold people are green.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If Dave is cold then Dave is not nice.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "nice" "-"))
If someone is cold then they are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and not nice then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "round" "+"))
If someone is round and not cold then they are not big.
((("someone" "is" "round" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "big" "-"))
All green, round people are kind.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and not big then they are kind.
((("someone" "is" "green" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "kind" "+"))
Dave is green.
True
1
proof
[(triple2 OR ((triple3 triple1) -> rule2) OR ((((triple1) -> rule4) triple1) -> rule2))]
("Dave" "is" "green" "+")
triple2
((triple3 triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Dave is not nice.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is round.
True
4
proof
[(((triple3 ((triple1) -> rule3)) -> rule5) OR ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5))]
("Dave" "is" "round" "+")
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not round.
False
4
inv-proof
[(((triple3 ((triple1) -> rule3)) -> rule5) OR ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5))]
("Dave" "is" "round" "-")
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is kind.
True
6
proof
[(((triple2 ((triple3 ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((triple2 ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((triple3 triple1) -> rule2) ((triple3 ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((triple3 triple1) -> rule2) ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((((triple1) -> rule4) triple1) -> rule2) ((triple3 ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((((triple1) -> rule4) triple1) -> rule2) ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5)) -> rule7))]
("Dave" "is" "kind" "+")
((triple2 ((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
((triple2 ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((triple3 triple1) -> (rule2 % int4)) ((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
((((triple3 triple1) -> (rule2 % int5)) ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
((((((triple1) -> (rule4 % int5)) triple1) -> (rule2 % int4)) ((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
((((((triple1) -> (rule4 % int5)) triple1) -> (rule2 % int4)) ((((triple1) -> (rule4 % int5)) ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
Dave is not kind.
False
6
inv-proof
[(((triple2 ((triple3 ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((triple2 ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((triple3 triple1) -> rule2) ((triple3 ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((triple3 triple1) -> rule2) ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((((triple1) -> rule4) triple1) -> rule2) ((triple3 ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((((triple1) -> rule4) triple1) -> rule2) ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5)) -> rule7))]
("Dave" "is" "kind" "-")
((triple2 ((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
((triple2 ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((triple3 triple1) -> (rule2 % int4)) ((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
((((triple3 triple1) -> (rule2 % int5)) ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
((((((triple1) -> (rule4 % int5)) triple1) -> (rule2 % int4)) ((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
((((((triple1) -> (rule4 % int5)) triple1) -> (rule2 % int4)) ((((triple1) -> (rule4 % int5)) ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
@0: Dave is cold.[(triple1)] Dave is green.[(triple2 OR ((triple3 triple1) -> rule2) OR ((((triple1) -> rule4) triple1) -> rule2))] Dave is rough.[(triple3 OR ((triple1) -> rule4))] @1: Dave is not nice.[(((triple1) -> rule3))] @2: Dave is round.[(((triple3 ((triple1) -> rule3)) -> rule5) OR ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5))] @3: Dave is kind.[(((triple2 ((triple3 ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((triple2 ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((triple3 triple1) -> rule2) ((triple3 ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((triple3 triple1) -> rule2) ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((((triple1) -> rule4) triple1) -> rule2) ((triple3 ((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((((triple1) -> rule4) triple1) -> rule2) ((((triple1) -> rule4) ((triple1) -> rule3)) -> rule5)) -> rule7))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple3 triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
((triple1) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((triple2 ((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
((triple2 ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((triple3 triple1) -> (rule2 % int4)) ((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
((((triple3 triple1) -> (rule2 % int5)) ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
int5
((((((triple1) -> (rule4 % int5)) triple1) -> (rule2 % int4)) ((triple3 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5
((((((triple1) -> (rule4 % int5)) triple1) -> (rule2 % int4)) ((((triple1) -> (rule4 % int5)) ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
("Dave" "is" "nice" "-")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5