Charlie is big. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is round. Charlie is white. Charlie is young. If something is quiet and red then it is young. If Charlie is nice and Charlie is white then Charlie is young. All round, white things are quiet. If something is white and young then it is big. All quiet, nice things are white. White things are quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If something is quiet and red then it is young.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Charlie is nice and Charlie is white then Charlie is young.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "young" "+"))
All round, white things are quiet.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is white and young then it is big.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All quiet, nice things are white.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
White things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Charlie is young.
True
1
proof
[(triple7 OR ((triple2 triple6) -> rule2) OR ((triple3 triple4) -> rule1) OR ((triple2 ((triple3 triple2) -> rule5)) -> rule2) OR ((((triple6) -> rule6) triple4) -> rule1) OR ((((triple5 triple6) -> rule3) triple4) -> rule1))]
("Charlie" "is" "young" "+")
triple7
((triple2 triple6) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple3 triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple2 ((triple3 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple6) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple5 triple6) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not white.
False
1
inv-proof
[(triple6 OR ((triple3 triple2) -> rule5))]
("Charlie" "is" "white" "-")
triple6
((triple3 triple2) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
@0: Charlie is big.[(triple1 OR ((triple6 triple7) -> rule4) OR ((triple6 ((triple2 triple6) -> rule2)) -> rule4) OR ((triple6 ((triple3 triple4) -> rule1)) -> rule4) OR ((((triple3 triple2) -> rule5) triple7) -> rule4) OR ((((triple3 triple2) -> rule5) ((triple2 triple6) -> rule2)) -> rule4) OR ((((triple3 triple2) -> rule5) ((triple3 triple4) -> rule1)) -> rule4) OR ((triple6 ((triple2 ((triple3 triple2) -> rule5)) -> rule2)) -> rule4) OR ((triple6 ((((triple6) -> rule6) triple4) -> rule1)) -> rule4) OR ((triple6 ((((triple5 triple6) -> rule3) triple4) -> rule1)) -> rule4) OR ((((triple3 triple2) -> rule5) ((triple2 ((triple3 triple2) -> rule5)) -> rule2)) -> rule4) OR ((((triple3 triple2) -> rule5) ((((triple6) -> rule6) triple4) -> rule1)) -> rule4) OR ((((triple3 triple2) -> rule5) ((((triple5 triple6) -> rule3) triple4) -> rule1)) -> rule4))] Charlie is nice.[(triple2)] Charlie is quiet.[(triple3 OR ((triple6) -> rule6) OR ((triple5 triple6) -> rule3))] Charlie is red.[(triple4)] Charlie is round.[(triple5)] Charlie is white.[(triple6 OR ((triple3 triple2) -> rule5))] Charlie is young.[(triple7 OR ((triple2 triple6) -> rule2) OR ((triple3 triple4) -> rule1) OR ((triple2 ((triple3 triple2) -> rule5)) -> rule2) OR ((((triple6) -> rule6) triple4) -> rule1) OR ((((triple5 triple6) -> rule3) triple4) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple6 triple7) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple6 ((triple2 triple6) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((triple6 ((triple3 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple3 triple2) -> (rule5 % int2)) triple7) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple3 triple2) -> (rule5 % int3)) ((triple2 triple6) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple3 triple2) -> (rule5 % int3)) ((triple3 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((triple6 ((triple2 ((triple3 triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((triple6 ((((triple6) -> (rule6 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((triple6 ((((triple5 triple6) -> (rule3 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple3 triple2) -> (rule5 % int3)) ((triple2 ((triple3 triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple3 triple2) -> (rule5 % int4)) ((((triple6) -> (rule6 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((triple3 triple2) -> (rule5 % int4)) ((((triple5 triple6) -> (rule3 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
((triple6) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((triple3 triple2) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple2 triple6) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple3 triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple2 ((triple3 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple6) -> (rule6 % int2)) triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple5 triple6) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2