Charlie is blue. Charlie is cold. Charlie is kind. Charlie is nice. Charlie is rough. Charlie is round. Charlie is young. Harry is blue. Harry is cold. Harry is kind. Harry is nice. Harry is not rough. Harry is round. Harry is young. If Harry is round then Harry is blue. If something is round then it is blue. If something is cold and not nice then it is blue. If Harry is blue and Harry is not cold then Harry is young. If something is round and not cold then it is rough. Kind things are young. Nice things are young. If Harry is blue then Harry is kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is round then Harry is blue.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "blue" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is cold and not nice then it is blue.
((("something" "is" "cold" "+") ("something" "is" "nice" "~")) -> ("something" "is" "blue" "+"))
If Harry is blue and Harry is not cold then Harry is young.
((("Harry" "is" "blue" "+") ("Harry" "is" "cold" "~")) -> ("Harry" "is" "young" "+"))
If something is round and not cold then it is rough.
((("something" "is" "round" "+") ("something" "is" "cold" "~")) -> ("something" "is" "rough" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Harry is blue then Harry is kind.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "kind" "+"))
Charlie is young.
True
1
proof
[(triple7 OR ((triple3) -> rule6) OR ((triple4) -> rule7))]
("Charlie" "is" "young" "+")
triple7
((triple3) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not kind.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "kind" "-")
triple3
@0: Charlie is blue.[(triple1 OR ((triple6) -> rule2))] Charlie is cold.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is rough.[(triple5)] Charlie is round.[(triple6)] Charlie is young.[(triple7 OR ((triple3) -> rule6) OR ((triple4) -> rule7))] Harry is blue.[(triple8 OR ((triple13) -> rule1) OR ((triple13) -> rule2))] Harry is cold.[(triple9)] Harry is kind.[(triple10 OR ((triple8) -> rule8) OR ((((triple13) -> rule1)) -> rule8) OR ((((triple13) -> rule2)) -> rule8))] Harry is nice.[(triple11)] Harry is not rough.[(triple12)] Harry is round.[(triple13)] Harry is young.[(triple14 OR ((triple10) -> rule6) OR ((triple11) -> rule7) OR ((((triple8) -> rule8)) -> rule6) OR ((((((triple13) -> rule1)) -> rule8)) -> rule6) OR ((((((triple13) -> rule2)) -> rule8)) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple6) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple3) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple8
((triple13) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple13) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
((triple8) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple13) -> (rule1 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple13) -> (rule2 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is not rough.
("Harry" "is" "rough" "-")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14
((triple10) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple11) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple8) -> (rule8 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple13) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple13) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3