Bob is cold. Bob is green. Bob is kind. Bob is quiet. Bob is rough. Bob is smart. Bob is young. Dave is cold. Dave is green. Dave is smart. Harry is cold. Harry is green. Harry is quiet. Harry is smart. Harry is young. Green people are young. All cold people are kind. Kind, smart people are rough. If Dave is smart and Dave is green then Dave is rough. If someone is quiet and kind then they are cold. Quiet people are kind. If Harry is young and Harry is quiet then Harry is smart. Green people are kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Kind, smart people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Dave is smart and Dave is green then Dave is rough.
((("Dave" "is" "smart" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "rough" "+"))
If someone is quiet and kind then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Harry is young and Harry is quiet then Harry is smart.
((("Harry" "is" "young" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "smart" "+"))
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Harry is quiet.
True
1
proof
[(triple13)]
("Harry" "is" "quiet" "+")
triple13
Bob is not smart.
False
1
inv-proof
[(triple6)]
("Bob" "is" "smart" "-")
triple6
@0: Bob is cold.[(triple1 OR ((triple4 triple3) -> rule5) OR ((triple4 ((triple2) -> rule8)) -> rule5) OR ((triple4 ((triple4) -> rule6)) -> rule5))] Bob is green.[(triple2)] Bob is kind.[(triple3 OR ((triple1) -> rule2) OR ((triple2) -> rule8) OR ((triple4) -> rule6))] Bob is quiet.[(triple4)] Bob is rough.[(triple5 OR ((triple3 triple6) -> rule3) OR ((((triple1) -> rule2) triple6) -> rule3) OR ((((triple2) -> rule8) triple6) -> rule3) OR ((((triple4) -> rule6) triple6) -> rule3))] Bob is smart.[(triple6)] Bob is young.[(triple7 OR ((triple2) -> rule1))] Dave is cold.[(triple8)] Dave is green.[(triple9)] Dave is smart.[(triple10)] Harry is cold.[(triple11 OR ((triple13 ((triple12) -> rule8)) -> rule5) OR ((triple13 ((triple13) -> rule6)) -> rule5))] Harry is green.[(triple12)] Harry is quiet.[(triple13)] Harry is smart.[(triple14 OR ((triple15 triple13) -> rule7) OR ((((triple12) -> rule1) triple13) -> rule7))] Harry is young.[(triple15 OR ((triple12) -> rule1))] @1: Dave is kind.[(((triple8) -> rule2) OR ((triple9) -> rule8))] Dave is rough.[(((triple10 triple9) -> rule4) OR ((((triple8) -> rule2) triple10) -> rule3) OR ((((triple9) -> rule8) triple10) -> rule3))] Dave is young.[(((triple9) -> rule1))] Harry is kind.[(((triple11) -> rule2) OR ((triple12) -> rule8) OR ((triple13) -> rule6))] @2: Harry is rough.[(((((triple11) -> rule2) triple14) -> rule3) OR ((((triple12) -> rule8) triple14) -> rule3) OR ((((triple13) -> rule6) triple14) -> rule3) OR ((((triple11) -> rule2) ((triple15 triple13) -> rule7)) -> rule3) OR ((((triple12) -> rule8) ((triple15 triple13) -> rule7)) -> rule3) OR ((((triple13) -> rule6) ((triple15 triple13) -> rule7)) -> rule3) OR ((((triple11) -> rule2) ((((triple12) -> rule1) triple13) -> rule7)) -> rule3) OR ((((triple12) -> rule8) ((((triple12) -> rule1) triple13) -> rule7)) -> rule3) OR ((((triple13) -> rule6) ((((triple12) -> rule1) triple13) -> rule7)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple4 triple3) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple4 ((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple4 ((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple1) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple4) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple3 triple6) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple2) -> (rule8 % int2)) triple6) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple4) -> (rule6 % int2)) triple6) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((triple13 ((triple12) -> (rule8 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((triple13 ((triple13) -> (rule6 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
((triple15 triple13) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple12) -> (rule1 % int2)) triple13) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple15
((triple12) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple8) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple9) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple10 triple9) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple8) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple9) -> (rule8 % int2)) triple10) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((triple9) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple11) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple12) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple13) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple11) -> (rule2 % int2)) triple14) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple12) -> (rule8 % int2)) triple14) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple13) -> (rule6 % int2)) triple14) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple11) -> (rule2 % int3)) ((triple15 triple13) -> (rule7 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((triple12) -> (rule8 % int3)) ((triple15 triple13) -> (rule7 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((triple13) -> (rule6 % int3)) ((triple15 triple13) -> (rule7 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((triple11) -> (rule2 % int4)) ((((triple12) -> (rule1 % int3)) triple13) -> (rule7 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((triple12) -> (rule8 % int4)) ((((triple12) -> (rule1 % int3)) triple13) -> (rule7 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((triple13) -> (rule6 % int4)) ((((triple12) -> (rule1 % int3)) triple13) -> (rule7 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4