Charlie is big. Charlie is quiet. Charlie is red. Charlie is rough. Charlie is round. Charlie is white. Harry is big. Harry is quiet. Harry is red. Harry is round. All quiet, round people are big. Quiet people are round. If someone is quiet and red then they are white. Rough people are big. If someone is young then they are rough. All quiet people are big. All red people are young. If someone is white then they are quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
All quiet, round people are big.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet and red then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is rough.
True
1
proof
[(triple4 OR ((((triple3) -> rule7)) -> rule5))]
("Charlie" "is" "rough" "+")
triple4
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not quiet.
False
1
inv-proof
[(triple2 OR ((triple6) -> rule8))]
("Charlie" "is" "quiet" "-")
triple2
((triple6) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Harry is young.
True
2
proof
[(((triple9) -> rule7))]
("Harry" "is" "young" "+")
((triple9) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not white.
False
3
inv-proof
[(((triple8 triple9) -> rule3))]
("Harry" "is" "white" "-")
((triple8 triple9) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
@0: Charlie is big.[(triple1 OR ((triple2) -> rule6) OR ((triple4) -> rule4) OR ((triple2 triple5) -> rule1) OR ((((triple6) -> rule8)) -> rule6) OR ((triple2 ((triple2) -> rule2)) -> rule1) OR ((((triple6) -> rule8) triple5) -> rule1) OR ((((triple6) -> rule8) ((triple2) -> rule2)) -> rule1) OR ((((((triple3) -> rule7)) -> rule5)) -> rule4) OR ((triple2 ((((triple6) -> rule8)) -> rule2)) -> rule1) OR ((((triple6) -> rule8) ((((triple6) -> rule8)) -> rule2)) -> rule1))] Charlie is quiet.[(triple2 OR ((triple6) -> rule8))] Charlie is red.[(triple3)] Charlie is rough.[(triple4 OR ((((triple3) -> rule7)) -> rule5))] Charlie is round.[(triple5 OR ((triple2) -> rule2) OR ((((triple6) -> rule8)) -> rule2))] Charlie is white.[(triple6 OR ((triple2 triple3) -> rule3))] Harry is big.[(triple7 OR ((triple8) -> rule6) OR ((triple8 triple10) -> rule1) OR ((triple8 ((triple8) -> rule2)) -> rule1) OR ((((((triple9) -> rule7)) -> rule5)) -> rule4))] Harry is quiet.[(triple8)] Harry is red.[(triple9)] Harry is round.[(triple10 OR ((triple8) -> rule2))] @1: Charlie is young.[(((triple3) -> rule7))] Harry is white.[(((triple8 triple9) -> rule3))] Harry is young.[(((triple9) -> rule7))] @2: Harry is rough.[(((((triple9) -> rule7)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple4) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple2 triple5) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple6) -> (rule8 % int2)) triple5) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple6) -> (rule8 % int3)) ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((triple2 ((((triple6) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple6) -> (rule8 % int3)) ((((triple6) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
((triple6) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple5
((triple2) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((triple2 triple3) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple8) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple8 triple10) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple8 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((((triple9) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
((triple8) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple8 triple9) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple9) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple9) -> (rule7 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2