Fiona is green. Fiona is quiet. Fiona is smart. If Fiona is white and Fiona is rough then Fiona is quiet. All rough, quiet people are round. If someone is smart and round then they are cold. Green people are rough. If someone is round then they are green. If someone is rough and smart then they are round. Cold people are white. All round people are rough.
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If Fiona is white and Fiona is rough then Fiona is quiet.
((("Fiona" "is" "white" "+") ("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "quiet" "+"))
All rough, quiet people are round.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is smart and round then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and smart then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Fiona is green.
True
1
proof
[(triple1)]
("Fiona" "is" "green" "+")
triple1
Fiona is not quiet.
False
1
inv-proof
[(triple2 OR ((((((triple3 ((((triple1) -> rule4) triple3) -> rule6)) -> rule3)) -> rule7) ((triple1) -> rule4)) -> rule1))]
("Fiona" "is" "quiet" "-")
triple2
((((((triple3 ((((triple1) -> (rule4 % int5)) triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int5))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
int5
Fiona is rough.
True
2
proof
[(((triple1) -> rule4))]
("Fiona" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("Fiona" "is" "rough" "-")
((triple1) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
@0: Fiona is green.[(triple1)] Fiona is quiet.[(triple2 OR ((((((triple3 ((((triple1) -> rule4) triple3) -> rule6)) -> rule3)) -> rule7) ((triple1) -> rule4)) -> rule1))] Fiona is smart.[(triple3)] @1: Fiona is rough.[(((triple1) -> rule4))] @2: Fiona is round.[(((((triple1) -> rule4) triple2) -> rule2) OR ((((triple1) -> rule4) triple3) -> rule6))] @3: Fiona is cold.[(((triple3 ((((triple1) -> rule4) triple2) -> rule2)) -> rule3) OR ((triple3 ((((triple1) -> rule4) triple3) -> rule6)) -> rule3))] @4: Fiona is white.[(((((triple3 ((((triple1) -> rule4) triple2) -> rule2)) -> rule3)) -> rule7) OR ((((triple3 ((((triple1) -> rule4) triple3) -> rule6)) -> rule3)) -> rule7))]
Fiona is green.
("Fiona" "is" "green" "+")
triple1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple2
((((((triple3 ((((triple1) -> (rule4 % int5)) triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int5))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
int5
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((((triple1) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((triple1) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple3 ((((triple1) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
((triple3 ((((triple1) -> (rule4 % int3)) triple3) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((((triple3 ((((triple1) -> (rule4 % int4)) triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
((((triple3 ((((triple1) -> (rule4 % int4)) triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4