Bob is not green. Erin is round. Fiona is round. Harry is not kind. If something is green then it is furry. Round, nice things are quiet. If Erin is quiet and Erin is blue then Erin is furry. If something is nice then it is not round. If Erin is nice and Erin is round then Erin is not green. Round things are blue. All round things are green. Furry things are not nice.
Bob is not green.
("Bob" "is" "green" "-")
Erin is round.
("Erin" "is" "round" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
If something is green then it is furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Round, nice things are quiet.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Erin is quiet and Erin is blue then Erin is furry.
((("Erin" "is" "quiet" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "furry" "+"))
If something is nice then it is not round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "-"))
If Erin is nice and Erin is round then Erin is not green.
((("Erin" "is" "nice" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "green" "-"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Furry things are not nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "-"))
Harry is not kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Erin is not round.
False
1
inv-proof
[(triple2)]
("Erin" "is" "round" "-")
triple2
Fiona is green.
True
2
proof
[(((triple3) -> rule7))]
("Fiona" "is" "green" "+")
((triple3) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple2) -> rule7))]
("Erin" "is" "green" "-")
((triple2) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Fiona is furry.
True
3
proof
[(((((triple3) -> rule7)) -> rule1))]
("Fiona" "is" "furry" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule1))]
("Erin" "is" "furry" "-")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Fiona is not nice.
True
4
proof
[(((((((triple3) -> rule7)) -> rule1)) -> rule8))]
("Fiona" "is" "nice" "-")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Erin is nice.
False
4
inv-proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule8))]
("Erin" "is" "nice" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Harry" "is" "furry" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Bob is not green.[(triple1)] Erin is round.[(triple2)] Fiona is round.[(triple3)] Harry is not kind.[(triple4)] @1: Erin is blue.[(((triple2) -> rule6))] Erin is green.[(((triple2) -> rule7))] Fiona is blue.[(((triple3) -> rule6))] Fiona is green.[(((triple3) -> rule7))] @2: Erin is furry.[(((((triple2) -> rule7)) -> rule1))] Fiona is furry.[(((((triple3) -> rule7)) -> rule1))] @3: Erin is not nice.[(((((((triple2) -> rule7)) -> rule1)) -> rule8))] Fiona is not nice.[(((((((triple3) -> rule7)) -> rule1)) -> rule8))]
Bob is not green.
("Bob" "is" "green" "-")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Harry is not kind.
("Harry" "is" "kind" "-")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple3) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Erin is not nice.
("Erin" "is" "nice" "-")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Fiona is not nice.
("Fiona" "is" "nice" "-")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3