Charlie is big. Charlie is quiet. Charlie is rough. Charlie is smart. Charlie is white. Harry is big. Harry is quiet. Harry is rough. Harry is round. Harry is smart. Harry is white. Harry is young. If something is white and rough then it is young. Big things are white. All round things are rough. If something is quiet and round then it is white. All quiet things are young. If something is quiet and big then it is white. All quiet, smart things are young. All white, quiet things are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is white and rough then it is young.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and round then it is white.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If something is quiet and big then it is white.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
All quiet, smart things are young.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All white, quiet things are smart.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Charlie is rough.
True
1
proof
[(triple3)]
("Charlie" "is" "rough" "+")
triple3
Harry is not round.
False
1
inv-proof
[(triple9)]
("Harry" "is" "round" "-")
triple9
@0: Charlie is big.[(triple1)] Charlie is quiet.[(triple2)] Charlie is rough.[(triple3)] Charlie is smart.[(triple4 OR ((triple5 triple2) -> rule8) OR ((((triple1) -> rule2) triple2) -> rule8) OR ((((triple2 triple1) -> rule6) triple2) -> rule8))] Charlie is white.[(triple5 OR ((triple1) -> rule2) OR ((triple2 triple1) -> rule6))] Harry is big.[(triple6)] Harry is quiet.[(triple7)] Harry is rough.[(triple8 OR ((triple9) -> rule3))] Harry is round.[(triple9)] Harry is smart.[(triple10 OR ((triple11 triple7) -> rule8) OR ((((triple6) -> rule2) triple7) -> rule8) OR ((((triple7 triple6) -> rule6) triple7) -> rule8) OR ((((triple7 triple9) -> rule4) triple7) -> rule8))] Harry is white.[(triple11 OR ((triple6) -> rule2) OR ((triple7 triple6) -> rule6) OR ((triple7 triple9) -> rule4))] Harry is young.[(triple12 OR ((triple7) -> rule5) OR ((triple11 triple8) -> rule1) OR ((triple7 triple10) -> rule7) OR ((triple11 ((triple9) -> rule3)) -> rule1) OR ((triple7 ((triple11 triple7) -> rule8)) -> rule7) OR ((((triple6) -> rule2) triple8) -> rule1) OR ((((triple7 triple6) -> rule6) triple8) -> rule1) OR ((((triple7 triple9) -> rule4) triple8) -> rule1) OR ((((triple6) -> rule2) ((triple9) -> rule3)) -> rule1) OR ((((triple7 triple6) -> rule6) ((triple9) -> rule3)) -> rule1) OR ((((triple7 triple9) -> rule4) ((triple9) -> rule3)) -> rule1) OR ((triple7 ((((triple6) -> rule2) triple7) -> rule8)) -> rule7) OR ((triple7 ((((triple7 triple6) -> rule6) triple7) -> rule8)) -> rule7) OR ((triple7 ((((triple7 triple9) -> rule4) triple7) -> rule8)) -> rule7))] @1: Charlie is young.[(((triple2) -> rule5) OR ((triple2 triple4) -> rule7) OR ((triple5 triple3) -> rule1) OR ((triple2 ((triple5 triple2) -> rule8)) -> rule7) OR ((((triple1) -> rule2) triple3) -> rule1) OR ((((triple2 triple1) -> rule6) triple3) -> rule1) OR ((triple2 ((((triple1) -> rule2) triple2) -> rule8)) -> rule7) OR ((triple2 ((((triple2 triple1) -> rule6) triple2) -> rule8)) -> rule7))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
((triple5 triple2) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple1) -> (rule2 % int2)) triple2) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple2 triple1) -> (rule6 % int2)) triple2) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple5
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple2 triple1) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
triple8
((triple9) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
((triple11 triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple6) -> (rule2 % int2)) triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple7 triple6) -> (rule6 % int2)) triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple7 triple9) -> (rule4 % int2)) triple7) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple11
((triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple7 triple6) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple7 triple9) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple7) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple11 triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple7 triple10) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple11 ((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple7 ((triple11 triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple6) -> (rule2 % int2)) triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple7 triple6) -> (rule6 % int2)) triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple7 triple9) -> (rule4 % int2)) triple8) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple7 triple6) -> (rule6 % int3)) ((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple7 triple9) -> (rule4 % int3)) ((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((triple7 ((((triple6) -> (rule2 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((triple7 ((((triple7 triple6) -> (rule6 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((triple7 ((((triple7 triple9) -> (rule4 % int3)) triple7) -> (rule8 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((triple2) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple2 triple4) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple5 triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple2 ((triple5 triple2) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((triple1) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple2 triple1) -> (rule6 % int2)) triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((triple2 ((((triple1) -> (rule2 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((triple2 ((((triple2 triple1) -> (rule6 % int3)) triple2) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3