Dave is big. Kind, cold people are smart. Green people are young. Blue, big people are kind. All big people are green. All young, big people are green. All green, big people are kind. All big people are cold. All kind, big people are young.
Dave is big.
("Dave" "is" "big" "+")
Kind, cold people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Blue, big people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All young, big people are green.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All green, big people are kind.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
All big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All kind, big people are young.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is green.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "green" "+")
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "green" "-")
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
True
3
proof
[(((((triple1) -> rule4)) -> rule2) OR ((((((triple1) -> rule4) triple1) -> rule6) triple1) -> rule8))]
("Dave" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((((triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple1) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not kind.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule6))]
("Dave" "is" "kind" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
@0: Dave is big.[(triple1)] @1: Dave is cold.[(((triple1) -> rule7))] Dave is green.[(((triple1) -> rule4))] @2: Dave is kind.[(((((triple1) -> rule4) triple1) -> rule6))] Dave is young.[(((((triple1) -> rule4)) -> rule2) OR ((((((triple1) -> rule4) triple1) -> rule6) triple1) -> rule8))] @3: Dave is smart.[(((((((triple1) -> rule4) triple1) -> rule6) ((triple1) -> rule7)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((((triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple1) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple1) -> (rule4 % int4)) triple1) -> (rule6 % int3)) ((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4