Anne is blue. Anne is green. Anne is quiet. Anne is rough. Anne is smart. Fiona is blue. Fiona is green. Fiona is nice. Fiona is quiet. Fiona is smart. If Anne is smart and Anne is kind then Anne is rough. Blue, quiet things are green. All smart, green things are rough. Smart things are kind. Kind things are green. If something is nice and blue then it is smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If Anne is smart and Anne is kind then Anne is rough.
((("Anne" "is" "smart" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "rough" "+"))
Blue, quiet things are green.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
All smart, green things are rough.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is nice and blue then it is smart.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Fiona is green.
True
1
proof
[(triple7 OR ((triple6 triple9) -> rule2) OR ((((triple10) -> rule4)) -> rule5) OR ((((((triple8 triple6) -> rule6)) -> rule4)) -> rule5))]
("Fiona" "is" "green" "+")
triple7
((triple6 triple9) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple8 triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is not smart.
False
1
inv-proof
[(triple10 OR ((triple8 triple6) -> rule6))]
("Fiona" "is" "smart" "-")
triple10
((triple8 triple6) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
True
3
proof
[(((triple10 triple7) -> rule3) OR ((triple10 ((triple6 triple9) -> rule2)) -> rule3) OR ((((triple8 triple6) -> rule6) triple7) -> rule3) OR ((((triple8 triple6) -> rule6) ((triple6 triple9) -> rule2)) -> rule3) OR ((triple10 ((((triple10) -> rule4)) -> rule5)) -> rule3) OR ((((triple8 triple6) -> rule6) ((((triple10) -> rule4)) -> rule5)) -> rule3) OR ((triple10 ((((((triple8 triple6) -> rule6)) -> rule4)) -> rule5)) -> rule3) OR ((((triple8 triple6) -> rule6) ((((((triple8 triple6) -> rule6)) -> rule4)) -> rule5)) -> rule3))]
("Fiona" "is" "rough" "+")
((triple10 triple7) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((triple10 ((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple8 triple6) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8 triple6) -> (rule6 % int3)) ((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((triple10 ((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((triple8 triple6) -> (rule6 % int4)) ((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((triple10 ((((((triple8 triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((((triple8 triple6) -> (rule6 % int4)) ((((((triple8 triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Anne is not kind.
False
2
inv-proof
[(((triple5) -> rule4))]
("Anne" "is" "kind" "-")
((triple5) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
@0: Anne is blue.[(triple1)] Anne is green.[(triple2 OR ((triple1 triple3) -> rule2) OR ((((triple5) -> rule4)) -> rule5))] Anne is quiet.[(triple3)] Anne is rough.[(triple4 OR ((triple5 triple2) -> rule3) OR ((triple5 ((triple5) -> rule4)) -> rule1) OR ((triple5 ((triple1 triple3) -> rule2)) -> rule3) OR ((triple5 ((((triple5) -> rule4)) -> rule5)) -> rule3))] Anne is smart.[(triple5)] Fiona is blue.[(triple6)] Fiona is green.[(triple7 OR ((triple6 triple9) -> rule2) OR ((((triple10) -> rule4)) -> rule5) OR ((((((triple8 triple6) -> rule6)) -> rule4)) -> rule5))] Fiona is nice.[(triple8)] Fiona is quiet.[(triple9)] Fiona is smart.[(triple10 OR ((triple8 triple6) -> rule6))] @1: Anne is kind.[(((triple5) -> rule4))] Fiona is kind.[(((triple10) -> rule4) OR ((((triple8 triple6) -> rule6)) -> rule4))] Fiona is rough.[(((triple10 triple7) -> rule3) OR ((triple10 ((triple6 triple9) -> rule2)) -> rule3) OR ((((triple8 triple6) -> rule6) triple7) -> rule3) OR ((((triple8 triple6) -> rule6) ((triple6 triple9) -> rule2)) -> rule3) OR ((triple10 ((((triple10) -> rule4)) -> rule5)) -> rule3) OR ((((triple8 triple6) -> rule6) ((((triple10) -> rule4)) -> rule5)) -> rule3) OR ((triple10 ((((((triple8 triple6) -> rule6)) -> rule4)) -> rule5)) -> rule3) OR ((((triple8 triple6) -> rule6) ((((((triple8 triple6) -> rule6)) -> rule4)) -> rule5)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1 triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple5 triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple5 ((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((triple5 ((triple1 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((triple5 ((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
((triple6 triple9) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple8 triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((triple8 triple6) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple5) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple10) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple8 triple6) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple10 triple7) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((triple10 ((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple8 triple6) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple8 triple6) -> (rule6 % int3)) ((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((triple10 ((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
((((triple8 triple6) -> (rule6 % int4)) ((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((triple10 ((((((triple8 triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((((triple8 triple6) -> (rule6 % int4)) ((((((triple8 triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4