Bob is not round. Charlie is blue. Charlie is green. Charlie is not round. Fiona is red. Harry is kind. Harry is not red. If something is red then it is kind. White things are kind. White, blue things are furry. All kind, blue things are furry. Kind, red things are white. If something is white then it is blue. If Harry is kind then Harry is white. If Harry is kind then Harry is round. All furry things are round.
Bob is not round.
("Bob" "is" "round" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not red.
("Harry" "is" "red" "-")
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
White things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
White, blue things are furry.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All kind, blue things are furry.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Kind, red things are white.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is white then it is blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If Harry is kind then Harry is white.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "white" "+"))
If Harry is kind then Harry is round.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "round" "+"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Charlie is not round.
True
1
proof
[(triple4)]
("Charlie" "is" "round" "-")
triple4
Charlie is round.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "round" "+")
triple4
Harry is round.
True
2
proof
[(((triple6) -> rule8) OR ((((triple6 ((((triple6) -> rule7)) -> rule6)) -> rule4)) -> rule9) OR ((((((triple6) -> rule7) ((((triple6) -> rule7)) -> rule6)) -> rule3)) -> rule9))]
("Harry" "is" "round" "+")
((triple6) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple6 ((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
((((((triple6) -> (rule7 % int4)) ((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is not round.
False
2
inv-proof
[(((triple6) -> rule8) OR ((((triple6 ((((triple6) -> rule7)) -> rule6)) -> rule4)) -> rule9) OR ((((((triple6) -> rule7) ((((triple6) -> rule7)) -> rule6)) -> rule3)) -> rule9))]
("Harry" "is" "round" "-")
((triple6) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple6 ((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
((((((triple6) -> (rule7 % int4)) ((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Fiona is white.
True
4
proof
[(((((triple5) -> rule1) triple5) -> rule5))]
("Fiona" "is" "white" "+")
((((triple5) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is not blue.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule6))]
("Harry" "is" "blue" "-")
((((triple6) -> (rule7 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is furry.
True
5
proof
[(((triple6 ((((triple6) -> rule7)) -> rule6)) -> rule4) OR ((((triple6) -> rule7) ((((triple6) -> rule7)) -> rule6)) -> rule3))]
("Harry" "is" "furry" "+")
((triple6 ((((triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple6) -> (rule7 % int3)) ((((triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Fiona is not blue.
False
5
inv-proof
[(((((((triple5) -> rule1) triple5) -> rule5)) -> rule6))]
("Fiona" "is" "blue" "-")
((((((triple5) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is furry.
True
8
proof
[(((((triple5) -> rule1) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule4) OR ((((((triple5) -> rule1) triple5) -> rule5) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule3))]
("Fiona" "is" "furry" "+")
((((triple5) -> (rule1 % int4)) ((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3)) ((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is not furry.
False
8
inv-proof
[(((((triple5) -> rule1) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule4) OR ((((((triple5) -> rule1) triple5) -> rule5) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule3))]
("Fiona" "is" "furry" "-")
((((triple5) -> (rule1 % int4)) ((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3)) ((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is round.
True
9
proof
[(((((((triple5) -> rule1) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule4)) -> rule9) OR ((((((((triple5) -> rule1) triple5) -> rule5) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule3)) -> rule9))]
("Fiona" "is" "round" "+")
((((((triple5) -> (rule1 % int5)) ((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
((((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4)) ((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Fiona is not round.
False
9
inv-proof
[(((((((triple5) -> rule1) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule4)) -> rule9) OR ((((((((triple5) -> rule1) triple5) -> rule5) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule3)) -> rule9))]
("Fiona" "is" "round" "-")
((((((triple5) -> (rule1 % int5)) ((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
((((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4)) ((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "kind" "+")
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is furry.
Unknown
rconc
[@3: Bob is furry.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule5 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Bob" "is" "blue" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "white" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is not round.[(triple1)] Charlie is blue.[(triple2)] Charlie is green.[(triple3)] Charlie is not round.[(triple4)] Fiona is red.[(triple5)] Harry is kind.[(triple6)] Harry is not red.[(triple7)] @1: Fiona is kind.[(((triple5) -> rule1))] Harry is round.[(((triple6) -> rule8) OR ((((triple6 ((((triple6) -> rule7)) -> rule6)) -> rule4)) -> rule9) OR ((((((triple6) -> rule7) ((((triple6) -> rule7)) -> rule6)) -> rule3)) -> rule9))] Harry is white.[(((triple6) -> rule7))] @2: Fiona is white.[(((((triple5) -> rule1) triple5) -> rule5))] Harry is blue.[(((((triple6) -> rule7)) -> rule6))] @3: Fiona is blue.[(((((((triple5) -> rule1) triple5) -> rule5)) -> rule6))] Harry is furry.[(((triple6 ((((triple6) -> rule7)) -> rule6)) -> rule4) OR ((((triple6) -> rule7) ((((triple6) -> rule7)) -> rule6)) -> rule3))] @4: Fiona is furry.[(((((triple5) -> rule1) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule4) OR ((((((triple5) -> rule1) triple5) -> rule5) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule3))] @5: Fiona is round.[(((((((triple5) -> rule1) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule4)) -> rule9) OR ((((((((triple5) -> rule1) triple5) -> rule5) ((((((triple5) -> rule1) triple5) -> rule5)) -> rule6)) -> rule3)) -> rule9))]
Bob is not round.
("Bob" "is" "round" "-")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is not round.
("Charlie" "is" "round" "-")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is not red.
("Harry" "is" "red" "-")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple6) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple6 ((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
((((((triple6) -> (rule7 % int4)) ((((triple6) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
((triple6) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((((triple5) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple6) -> (rule7 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((triple5) -> (rule1 % int3)) triple5) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((triple6 ((((triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple6) -> (rule7 % int3)) ((((triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple5) -> (rule1 % int4)) ((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3)) ((((((triple5) -> (rule1 % int4)) triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
((((((triple5) -> (rule1 % int5)) ((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
((((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4)) ((((((triple5) -> (rule1 % int5)) triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule9 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5