Dave is nice. All blue things are big. If Dave is nice and Dave is rough then Dave is blue. All nice things are rough. If Dave is cold and Dave is nice then Dave is red. Blue things are kind. All kind, rough things are big. If Dave is red and Dave is cold then Dave is nice. Rough, big things are red.
Dave is nice.
("Dave" "is" "nice" "+")
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If Dave is nice and Dave is rough then Dave is blue.
((("Dave" "is" "nice" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "blue" "+"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Dave is cold and Dave is nice then Dave is red.
((("Dave" "is" "cold" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "red" "+"))
Blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All kind, rough things are big.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If Dave is red and Dave is cold then Dave is nice.
((("Dave" "is" "red" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "nice" "+"))
Rough, big things are red.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Dave is nice.
True
1
proof
[(triple1)]
("Dave" "is" "nice" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple1)]
("Dave" "is" "nice" "-")
triple1
Dave is rough.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("Dave" "is" "blue" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("Dave" "is" "blue" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
True
5
proof
[(((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1) OR ((((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule5) ((triple1) -> rule3)) -> rule6))]
("Dave" "is" "big" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int4))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is not big.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1) OR ((((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule5) ((triple1) -> rule3)) -> rule6))]
("Dave" "is" "big" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int4))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
@0: Dave is nice.[(triple1)] @1: Dave is rough.[(((triple1) -> rule3))] @2: Dave is blue.[(((triple1 ((triple1) -> rule3)) -> rule2))] @3: Dave is big.[(((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1) OR ((((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule5) ((triple1) -> rule3)) -> rule6))] Dave is kind.[(((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule5))] @4: Dave is red.[(((((triple1) -> rule3) ((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1)) -> rule8) OR ((((triple1) -> rule3) ((((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule5) ((triple1) -> rule3)) -> rule6)) -> rule8))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule3 % int4))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule3 % int4)) ((((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
((((triple1) -> (rule3 % int5)) ((((((triple1 ((triple1) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3)) ((triple1) -> (rule3 % int5))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is rough.
("Dave" "is" "rough" "+")
int5