Charlie is big. Charlie is blue. Charlie is quiet. Charlie is red. Charlie is smart. Harry is big. Harry is blue. Harry is kind. Harry is quiet. Harry is red. Harry is rough. Harry is smart. If Charlie is rough then Charlie is kind. If Harry is rough and Harry is red then Harry is blue. If Harry is kind and Harry is blue then Harry is quiet. If something is big and quiet then it is rough. If something is red and big then it is rough. If Charlie is kind then Charlie is red.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Charlie is rough then Charlie is kind.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "kind" "+"))
If Harry is rough and Harry is red then Harry is blue.
((("Harry" "is" "rough" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is kind and Harry is blue then Harry is quiet.
((("Harry" "is" "kind" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "quiet" "+"))
If something is big and quiet then it is rough.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is red and big then it is rough.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If Charlie is kind then Charlie is red.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "red" "+"))
Harry is kind.
True
1
proof
[(triple8)]
("Harry" "is" "kind" "+")
triple8
Charlie is not red.
False
1
inv-proof
[(triple4 OR ((((((triple1 triple3) -> rule4)) -> rule1)) -> rule6))]
("Charlie" "is" "red" "-")
triple4
((((((triple1 triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is rough.
True
3
proof
[(((triple1 triple3) -> rule4) OR ((triple4 triple1) -> rule5))]
("Charlie" "is" "rough" "+")
((triple1 triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4 triple1) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
3
inv-proof
[(((triple1 triple3) -> rule4) OR ((triple4 triple1) -> rule5))]
("Charlie" "is" "rough" "-")
((triple1 triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4 triple1) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is quiet.[(triple3)] Charlie is red.[(triple4 OR ((((((triple1 triple3) -> rule4)) -> rule1)) -> rule6))] Charlie is smart.[(triple5)] Harry is big.[(triple6)] Harry is blue.[(triple7 OR ((triple11 triple10) -> rule2) OR ((((triple10 triple6) -> rule5) triple10) -> rule2) OR ((((triple6 triple9) -> rule4) triple10) -> rule2))] Harry is kind.[(triple8)] Harry is quiet.[(triple9 OR ((triple8 triple7) -> rule3) OR ((triple8 ((triple11 triple10) -> rule2)) -> rule3) OR ((triple8 ((((triple10 triple6) -> rule5) triple10) -> rule2)) -> rule3))] Harry is red.[(triple10)] Harry is rough.[(triple11 OR ((triple10 triple6) -> rule5) OR ((triple6 triple9) -> rule4) OR ((triple6 ((triple8 triple7) -> rule3)) -> rule4))] Harry is smart.[(triple12)] @1: Charlie is rough.[(((triple1 triple3) -> rule4) OR ((triple4 triple1) -> rule5))] @2: Charlie is kind.[(((((triple1 triple3) -> rule4)) -> rule1) OR ((((triple4 triple1) -> rule5)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((((((triple1 triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
((triple11 triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple10 triple6) -> (rule5 % int2)) triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple6 triple9) -> (rule4 % int2)) triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
((triple8 triple7) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple8 ((triple11 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((triple8 ((((triple10 triple6) -> (rule5 % int3)) triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((triple10 triple6) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple6 triple9) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple6 ((triple8 triple7) -> (rule3 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1 triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4 triple1) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple1 triple3) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple4 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2