Fiona is big. Harry is round. If Harry is furry and Harry is rough then Harry is blue. If Harry is big and Harry is not blue then Harry is not green. Blue, quiet things are not big. All blue things are big. All big things are green. If something is quiet and rough then it is round. Green things are quiet. If Harry is round and Harry is not rough then Harry is quiet.
Fiona is big.
("Fiona" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is furry and Harry is rough then Harry is blue.
((("Harry" "is" "furry" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is big and Harry is not blue then Harry is not green.
((("Harry" "is" "big" "+") ("Harry" "is" "blue" "~")) -> ("Harry" "is" "green" "-"))
Blue, quiet things are not big.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "-"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is quiet and rough then it is round.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If Harry is round and Harry is not rough then Harry is quiet.
((("Harry" "is" "round" "+") ("Harry" "is" "rough" "~")) -> ("Harry" "is" "quiet" "+"))
Fiona is big.
True
1
proof
[(triple1)]
("Fiona" "is" "big" "+")
triple1
Fiona is not big.
False
1
inv-proof
[(triple1)]
("Fiona" "is" "big" "-")
triple1
Fiona is green.
True
2
proof
[(((triple1) -> rule5))]
("Fiona" "is" "green" "+")
((triple1) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Fiona" "is" "green" "-")
((triple1) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple1) -> rule5)) -> rule7))]
("Fiona" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not quiet.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule7))]
("Fiona" "is" "quiet" "-")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "round" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not quiet.
Unknown
inv-rconc
[@4: Harry is quiet.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule4 <- rule1 <- FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Fiona is big.[(triple1)] Harry is round.[(triple2)] @1: Fiona is green.[(((triple1) -> rule5))] @2: Fiona is quiet.[(((((triple1) -> rule5)) -> rule7))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
Harry is round.
("Harry" "is" "round" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
((triple1) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2