Bob is blue. Bob is green. Bob is kind. Bob is nice. Bob is rough. Bob is round. Bob is young. Dave is blue. Dave is green. Dave is nice. Dave is rough. Dave is round. Dave is young. Erin is blue. Erin is green. Erin is nice. Round, green things are kind. If Erin is rough then Erin is round. All kind, young things are nice. Green things are rough. If something is rough and round then it is blue. All nice things are rough.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Round, green things are kind.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If Erin is rough then Erin is round.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "round" "+"))
All kind, young things are nice.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is rough and round then it is blue.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Dave is round.
True
1
proof
[(triple12)]
("Dave" "is" "round" "+")
triple12
Dave is not blue.
False
1
inv-proof
[(triple8 OR ((triple11 triple12) -> rule5) OR ((((triple10) -> rule6) triple12) -> rule5) OR ((((triple9) -> rule4) triple12) -> rule5) OR ((((((((triple12 triple9) -> rule1) triple13) -> rule3)) -> rule6) triple12) -> rule5))]
("Dave" "is" "blue" "-")
triple8
((triple11 triple12) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple10) -> (rule6 % int2)) triple12) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple9) -> (rule4 % int2)) triple12) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((((((triple12 triple9) -> (rule1 % int4)) triple13) -> (rule3 % int3))) -> (rule6 % int2)) triple12) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Erin is rough.
True
2
proof
[(((triple15) -> rule4) OR ((triple16) -> rule6))]
("Erin" "is" "rough" "+")
((triple15) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple16) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple15) -> rule4) OR ((triple16) -> rule6))]
("Erin" "is" "rough" "-")
((triple15) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple16) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
True
3
proof
[(((((triple15) -> rule4)) -> rule2) OR ((((triple16) -> rule6)) -> rule2))]
("Erin" "is" "round" "+")
((((triple15) -> (rule4 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple16) -> (rule6 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple15) -> rule4)) -> rule2) OR ((((triple16) -> rule6)) -> rule2))]
("Erin" "is" "round" "-")
((((triple15) -> (rule4 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple16) -> (rule6 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
True
5
proof
[(((((((triple15) -> rule4)) -> rule2) triple15) -> rule1) OR ((((((triple16) -> rule6)) -> rule2) triple15) -> rule1))]
("Erin" "is" "kind" "+")
((((((triple15) -> (rule4 % int3))) -> (rule2 % int2)) triple15) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple16) -> (rule6 % int3))) -> (rule2 % int2)) triple15) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not kind.
False
5
inv-proof
[(((((((triple15) -> rule4)) -> rule2) triple15) -> rule1) OR ((((((triple16) -> rule6)) -> rule2) triple15) -> rule1))]
("Erin" "is" "kind" "-")
((((((triple15) -> (rule4 % int3))) -> (rule2 % int2)) triple15) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple16) -> (rule6 % int3))) -> (rule2 % int2)) triple15) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
@0: Bob is blue.[(triple1 OR ((triple5 triple6) -> rule5) OR ((((triple2) -> rule4) triple6) -> rule5) OR ((((triple4) -> rule6) triple6) -> rule5) OR ((((((triple3 triple7) -> rule3)) -> rule6) triple6) -> rule5) OR ((((((((triple6 triple2) -> rule1) triple7) -> rule3)) -> rule6) triple6) -> rule5))] Bob is green.[(triple2)] Bob is kind.[(triple3 OR ((triple6 triple2) -> rule1))] Bob is nice.[(triple4 OR ((triple3 triple7) -> rule3) OR ((((triple6 triple2) -> rule1) triple7) -> rule3))] Bob is rough.[(triple5 OR ((triple2) -> rule4) OR ((triple4) -> rule6) OR ((((triple3 triple7) -> rule3)) -> rule6) OR ((((((triple6 triple2) -> rule1) triple7) -> rule3)) -> rule6))] Bob is round.[(triple6)] Bob is young.[(triple7)] Dave is blue.[(triple8 OR ((triple11 triple12) -> rule5) OR ((((triple10) -> rule6) triple12) -> rule5) OR ((((triple9) -> rule4) triple12) -> rule5) OR ((((((((triple12 triple9) -> rule1) triple13) -> rule3)) -> rule6) triple12) -> rule5))] Dave is green.[(triple9)] Dave is nice.[(triple10 OR ((((triple12 triple9) -> rule1) triple13) -> rule3))] Dave is rough.[(triple11 OR ((triple10) -> rule6) OR ((triple9) -> rule4) OR ((((((triple12 triple9) -> rule1) triple13) -> rule3)) -> rule6))] Dave is round.[(triple12)] Dave is young.[(triple13)] Erin is blue.[(triple14 OR ((((triple15) -> rule4) ((((triple15) -> rule4)) -> rule2)) -> rule5) OR ((((triple15) -> rule4) ((((triple16) -> rule6)) -> rule2)) -> rule5) OR ((((triple16) -> rule6) ((((triple15) -> rule4)) -> rule2)) -> rule5) OR ((((triple16) -> rule6) ((((triple16) -> rule6)) -> rule2)) -> rule5))] Erin is green.[(triple15)] Erin is nice.[(triple16)] @1: Dave is kind.[(((triple12 triple9) -> rule1))] Erin is rough.[(((triple15) -> rule4) OR ((triple16) -> rule6))] @2: Erin is round.[(((((triple15) -> rule4)) -> rule2) OR ((((triple16) -> rule6)) -> rule2))] @3: Erin is kind.[(((((((triple15) -> rule4)) -> rule2) triple15) -> rule1) OR ((((((triple16) -> rule6)) -> rule2) triple15) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple5 triple6) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple2) -> (rule4 % int2)) triple6) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple4) -> (rule6 % int2)) triple6) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple3 triple7) -> (rule3 % int3))) -> (rule6 % int2)) triple6) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((((triple6 triple2) -> (rule1 % int4)) triple7) -> (rule3 % int3))) -> (rule6 % int2)) triple6) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple6 triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple3 triple7) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple6 triple2) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple2) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple4) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3 triple7) -> (rule3 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple6 triple2) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
((triple11 triple12) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple10) -> (rule6 % int2)) triple12) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple9) -> (rule4 % int2)) triple12) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((((((triple12 triple9) -> (rule1 % int4)) triple13) -> (rule3 % int3))) -> (rule6 % int2)) triple12) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
((((triple12 triple9) -> (rule1 % int2)) triple13) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple11
((triple10) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple9) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((((triple12 triple9) -> (rule1 % int3)) triple13) -> (rule3 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple12
Dave is young.
("Dave" "is" "young" "+")
triple13
Erin is blue.
("Erin" "is" "blue" "+")
triple14
((((triple15) -> (rule4 % int3)) ((((triple15) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((triple15) -> (rule4 % int3)) ((((triple16) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((triple16) -> (rule6 % int3)) ((((triple15) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((triple16) -> (rule6 % int3)) ((((triple16) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple15
Erin is nice.
("Erin" "is" "nice" "+")
triple16
Dave is kind.
("Dave" "is" "kind" "+")
((triple12 triple9) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple15) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple16) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple15) -> (rule4 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple16) -> (rule6 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple15) -> (rule4 % int3))) -> (rule2 % int2)) triple15) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple16) -> (rule6 % int3))) -> (rule2 % int2)) triple15) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3