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