Charlie is furry. Charlie is rough. Dave is blue. Dave is furry. Dave is white. Erin is nice. Erin is rough. Erin is smart. Harry is blue. Harry is cold. Harry is furry. Harry is white. White, nice things are rough. All cold, smart things are white. If something is white and rough then it is nice. Rough things are smart. All furry, blue things are nice. All nice, rough things are cold. If something is smart then it is blue.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is white.
("Harry" "is" "white" "+")
White, nice things are rough.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All cold, smart things are white.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is white and rough then it is nice.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All furry, blue things are nice.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
All nice, rough things are cold.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Harry is white.
True
1
proof
[(triple12)]
("Harry" "is" "white" "+")
triple12
Harry is not furry.
False
1
inv-proof
[(triple11)]
("Harry" "is" "furry" "-")
triple11
Erin is blue.
True
2
proof
[(((triple8) -> rule7) OR ((((triple7) -> rule4)) -> rule7))]
("Erin" "is" "blue" "+")
((triple8) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Charlie is not smart.
False
2
inv-proof
[(((triple2) -> rule4))]
("Charlie" "is" "smart" "-")
((triple2) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is rough.
True
5
proof
[(((triple12 ((triple11 triple9) -> rule5)) -> rule1))]
("Harry" "is" "rough" "+")
((triple12 ((triple11 triple9) -> (rule5 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Erin is not white.
False
5
inv-proof
[(((((triple6 triple7) -> rule6) triple8) -> rule2) OR ((((triple6 triple7) -> rule6) ((triple7) -> rule4)) -> rule2))]
("Erin" "is" "white" "-")
((((triple6 triple7) -> (rule6 % int2)) triple8) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple6 triple7) -> (rule6 % int3)) ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Charlie is nice.
True
5
proof
[(((triple1 ((((triple2) -> rule4)) -> rule7)) -> rule5))]
("Charlie" "is" "nice" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Harry is not smart.
False
6
inv-proof
[(((((triple12 ((triple11 triple9) -> rule5)) -> rule1)) -> rule4))]
("Harry" "is" "smart" "-")
((((triple12 ((triple11 triple9) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Charlie is cold.
True
7
proof
[(((((triple1 ((((triple2) -> rule4)) -> rule7)) -> rule5) triple2) -> rule6))]
("Charlie" "is" "cold" "+")
((((triple1 ((((triple2) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is not cold.
False
7
inv-proof
[(((((triple1 ((((triple2) -> rule4)) -> rule7)) -> rule5) triple2) -> rule6))]
("Charlie" "is" "cold" "-")
((((triple1 ((((triple2) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is white.
True
10
proof
[(((((((triple1 ((((triple2) -> rule4)) -> rule7)) -> rule5) triple2) -> rule6) ((triple2) -> rule4)) -> rule2))]
("Charlie" "is" "white" "+")
((((((triple1 ((((triple2) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) triple2) -> (rule6 % int2)) ((triple2) -> (rule4 % int5))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5
Charlie is not white.
False
10
inv-proof
[(((((((triple1 ((((triple2) -> rule4)) -> rule7)) -> rule5) triple2) -> rule6) ((triple2) -> rule4)) -> rule2))]
("Charlie" "is" "white" "-")
((((((triple1 ((((triple2) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) triple2) -> (rule6 % int2)) ((triple2) -> (rule4 % int5))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5
@0: Charlie is furry.[(triple1)] Charlie is rough.[(triple2)] Dave is blue.[(triple3)] Dave is furry.[(triple4)] Dave is white.[(triple5)] Erin is nice.[(triple6)] Erin is rough.[(triple7)] Erin is smart.[(triple8 OR ((triple7) -> rule4))] Harry is blue.[(triple9)] Harry is cold.[(triple10 OR ((((triple11 triple9) -> rule5) ((triple12 ((triple11 triple9) -> rule5)) -> rule1)) -> rule6))] Harry is furry.[(triple11)] Harry is white.[(triple12)] @1: Charlie is smart.[(((triple2) -> rule4))] Dave is nice.[(((triple4 triple3) -> rule5))] Erin is blue.[(((triple8) -> rule7) OR ((((triple7) -> rule4)) -> rule7))] Erin is cold.[(((triple6 triple7) -> rule6))] Harry is nice.[(((triple11 triple9) -> rule5))] @2: Charlie is blue.[(((((triple2) -> rule4)) -> rule7))] Dave is rough.[(((triple5 ((triple4 triple3) -> rule5)) -> rule1))] Erin is white.[(((((triple6 triple7) -> rule6) triple8) -> rule2) OR ((((triple6 triple7) -> rule6) ((triple7) -> rule4)) -> rule2))] Harry is rough.[(((triple12 ((triple11 triple9) -> rule5)) -> rule1))] @3: Charlie is nice.[(((triple1 ((((triple2) -> rule4)) -> rule7)) -> rule5))] Dave is cold.[(((((triple4 triple3) -> rule5) ((triple5 ((triple4 triple3) -> rule5)) -> rule1)) -> rule6))] Dave is smart.[(((((triple5 ((triple4 triple3) -> rule5)) -> rule1)) -> rule4))] Harry is smart.[(((((triple12 ((triple11 triple9) -> rule5)) -> rule1)) -> rule4))] @4: Charlie is cold.[(((((triple1 ((((triple2) -> rule4)) -> rule7)) -> rule5) triple2) -> rule6))] @5: Charlie is white.[(((((((triple1 ((((triple2) -> rule4)) -> rule7)) -> rule5) triple2) -> rule6) ((triple2) -> rule4)) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
((triple7) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
((((triple11 triple9) -> (rule5 % int3)) ((triple12 ((triple11 triple9) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple4 triple3) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple8) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple6 triple7) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple11 triple9) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple5 ((triple4 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple6 triple7) -> (rule6 % int2)) triple8) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple6 triple7) -> (rule6 % int3)) ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((triple12 ((triple11 triple9) -> (rule5 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((triple4 triple3) -> (rule5 % int3)) ((triple5 ((triple4 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((triple5 ((triple4 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((triple12 ((triple11 triple9) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1 ((((triple2) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple1 ((((triple2) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule5 % int3)) triple2) -> (rule6 % int2)) ((triple2) -> (rule4 % int5))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
int5