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