Fiona is cold. If Fiona is green and Fiona is young then Fiona is nice. Young things are not green. If something is nice then it is green. If something is rough then it is not round. Cold things are quiet. All cold, quiet things are young. Young things are cold. All nice things are cold.
Fiona is cold.
("Fiona" "is" "cold" "+")
If Fiona is green and Fiona is young then Fiona is nice.
((("Fiona" "is" "green" "+") ("Fiona" "is" "young" "+")) -> ("Fiona" "is" "nice" "+"))
Young things are not green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "-"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is rough then it is not round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "-"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All cold, quiet things are young.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Fiona is cold.
True
1
proof
[(triple1)]
("Fiona" "is" "cold" "+")
triple1
Fiona is not cold.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "cold" "-")
triple1
Fiona is quiet.
True
2
proof
[(((triple1) -> rule5))]
("Fiona" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Fiona" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("Fiona" "is" "young" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("Fiona" "is" "young" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not green.
True
5
proof
[(((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
("Fiona" "is" "green" "-")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is green.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
("Fiona" "is" "green" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Fiona is cold.[(triple1)] @1: Fiona is quiet.[(((triple1) -> rule5))] @2: Fiona is young.[(((triple1 ((triple1) -> rule5)) -> rule6))] @3: Fiona is not green.[(((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
Fiona is cold.
("Fiona" "is" "cold" "+")
triple1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not green.
("Fiona" "is" "green" "-")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3