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