Charlie is kind. Charlie is nice. Charlie is red. Charlie is round. Charlie is young. Erin is kind. Erin is nice. Erin is red. Erin is rough. Erin is round. Erin is white. Erin is not young. If Charlie is round then Charlie is rough. Red, young people are nice. All red, rough people are nice. If someone is kind then they are white. If Charlie is nice and Charlie is red then Charlie is kind. If Charlie is white and Charlie is kind then Charlie is young. If someone is kind then they are round. All nice, red people are round.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is not young.
("Erin" "is" "young" "-")
If Charlie is round then Charlie is rough.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "rough" "+"))
Red, young people are nice.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All red, rough people are nice.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If Charlie is nice and Charlie is red then Charlie is kind.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "kind" "+"))
If Charlie is white and Charlie is kind then Charlie is young.
((("Charlie" "is" "white" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "young" "+"))
If someone is kind then they are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
All nice, red people are round.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Charlie is young.
True
1
proof
[(triple5 OR ((((triple1) -> rule4) triple1) -> rule6) OR ((((triple1) -> rule4) ((triple2 triple3) -> rule5)) -> rule6) OR ((((((triple2 triple3) -> rule5)) -> rule4) triple1) -> rule6) OR ((((((triple2 triple3) -> rule5)) -> rule4) ((triple2 triple3) -> rule5)) -> rule6) OR ((((triple1) -> rule4) ((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule6) OR ((((((triple2 triple3) -> rule5)) -> rule4) ((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule6) OR ((((((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule4) triple1) -> rule6) OR ((((((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule4) ((triple2 triple3) -> rule5)) -> rule6) OR ((((((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule4) ((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule6))]
("Charlie" "is" "young" "+")
triple5
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple2 triple3) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple2 triple3) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple2 triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple2 triple3) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple1) -> (rule4 % int5)) ((((triple3 ((triple4) -> (rule1 % int4))) -> (rule3 % int3)) triple3) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5
((((((triple2 triple3) -> (rule5 % int5))) -> (rule4 % int4)) ((((triple3 ((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule5 % int5))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
((((((((triple3 ((triple4) -> (rule1 % int5))) -> (rule3 % int4)) triple3) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
((((((((triple3 ((triple4) -> (rule1 % int5))) -> (rule3 % int4)) triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple2 triple3) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
((((((((triple3 ((triple4) -> (rule1 % int5))) -> (rule3 % int4)) triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((((triple3 ((triple4) -> (rule1 % int5))) -> (rule3 % int4)) triple3) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
Charlie is not red.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "red" "-")
triple3
@0: Charlie is kind.[(triple1 OR ((triple2 triple3) -> rule5) OR ((((triple3 triple5) -> rule2) triple3) -> rule5) OR ((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5))] Charlie is nice.[(triple2 OR ((triple3 triple5) -> rule2) OR ((triple3 ((triple4) -> rule1)) -> rule3) OR ((triple3 ((((triple1) -> rule7)) -> rule1)) -> rule3) OR ((triple3 ((((triple1) -> rule4) triple1) -> rule6)) -> rule2))] Charlie is red.[(triple3)] Charlie is round.[(triple4 OR ((triple1) -> rule7) OR ((triple2 triple3) -> rule8) OR ((((triple2 triple3) -> rule5)) -> rule7) OR ((((triple3 triple5) -> rule2) triple3) -> rule8) OR ((((((triple3 triple5) -> rule2) triple3) -> rule5)) -> rule7) OR ((((triple3 ((((triple1) -> rule4) triple1) -> rule6)) -> rule2) triple3) -> rule8))] Charlie is young.[(triple5 OR ((((triple1) -> rule4) triple1) -> rule6) OR ((((triple1) -> rule4) ((triple2 triple3) -> rule5)) -> rule6) OR ((((((triple2 triple3) -> rule5)) -> rule4) triple1) -> rule6) OR ((((((triple2 triple3) -> rule5)) -> rule4) ((triple2 triple3) -> rule5)) -> rule6) OR ((((triple1) -> rule4) ((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule6) OR ((((((triple2 triple3) -> rule5)) -> rule4) ((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule6) OR ((((((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule4) triple1) -> rule6) OR ((((((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule4) ((triple2 triple3) -> rule5)) -> rule6) OR ((((((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule4) ((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule6))] Erin is kind.[(triple6)] Erin is nice.[(triple7 OR ((triple8 triple9) -> rule3))] Erin is not young.[(triple12)] Erin is red.[(triple8)] Erin is rough.[(triple9)] Erin is round.[(triple10 OR ((triple6) -> rule7) OR ((triple7 triple8) -> rule8) OR ((((triple8 triple9) -> rule3) triple8) -> rule8))] Erin is white.[(triple11 OR ((triple6) -> rule4))] @1: Charlie is rough.[(((triple4) -> rule1) OR ((((triple1) -> rule7)) -> rule1) OR ((((triple2 triple3) -> rule8)) -> rule1) OR ((((((triple2 triple3) -> rule5)) -> rule7)) -> rule1) OR ((((((triple3 triple5) -> rule2) triple3) -> rule8)) -> rule1) OR ((((((((triple3 triple5) -> rule2) triple3) -> rule5)) -> rule7)) -> rule1) OR ((((((triple3 ((((triple1) -> rule4) triple1) -> rule6)) -> rule2) triple3) -> rule8)) -> rule1))] Charlie is white.[(((triple1) -> rule4) OR ((((triple2 triple3) -> rule5)) -> rule4) OR ((((((triple3 triple5) -> rule2) triple3) -> rule5)) -> rule4) OR ((((((triple3 ((triple4) -> rule1)) -> rule3) triple3) -> rule5)) -> rule4))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
((triple2 triple3) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple3 triple5) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple3 ((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
((triple3 triple5) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple3 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((triple3 ((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((triple3 ((((triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
((triple1) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple2 triple3) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple2 triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple3 triple5) -> (rule2 % int2)) triple3) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((((triple3 triple5) -> (rule2 % int3)) triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((triple3 ((((triple1) -> (rule4 % int4)) triple1) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple2 triple3) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple2 triple3) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple2 triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple2 triple3) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple1) -> (rule4 % int5)) ((((triple3 ((triple4) -> (rule1 % int4))) -> (rule3 % int3)) triple3) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5
((((((triple2 triple3) -> (rule5 % int5))) -> (rule4 % int4)) ((((triple3 ((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule5 % int5))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
((((((((triple3 ((triple4) -> (rule1 % int5))) -> (rule3 % int4)) triple3) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
((((((((triple3 ((triple4) -> (rule1 % int5))) -> (rule3 % int4)) triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple2 triple3) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
((((((((triple3 ((triple4) -> (rule1 % int5))) -> (rule3 % int4)) triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((((triple3 ((triple4) -> (rule1 % int5))) -> (rule3 % int4)) triple3) -> (rule5 % int3))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
((triple8 triple9) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
triple12
Erin is red.
("Erin" "is" "red" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple10
((triple6) -> (rule7 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple7 triple8) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple8 triple9) -> (rule3 % int2)) triple8) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple11
((triple6) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple2 triple3) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((triple2 triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple3 triple5) -> (rule2 % int3)) triple3) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((((triple3 triple5) -> (rule2 % int4)) triple3) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
((((((triple3 ((((triple1) -> (rule4 % int5)) triple1) -> (rule6 % int4))) -> (rule2 % int3)) triple3) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
int5
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple2 triple3) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple3 triple5) -> (rule2 % int3)) triple3) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple3 ((triple4) -> (rule1 % int4))) -> (rule3 % int3)) triple3) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4