Bob is kind. Bob is nice. Bob is white. Charlie is white. Charlie is young. Dave is blue. Dave is furry. Dave is nice. Dave is red. Dave is white. Dave is young. Erin is blue. Erin is kind. Erin is red. Erin is young. If Charlie is red then Charlie is furry. If Dave is red and Dave is kind then Dave is white. If Erin is not white then Erin is nice. Kind, young people are furry. If someone is red and not blue then they are furry. If someone is furry and blue then they are nice. White people are red. Red, white people are young.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
If Charlie is red then Charlie is furry.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "furry" "+"))
If Dave is red and Dave is kind then Dave is white.
((("Dave" "is" "red" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "white" "+"))
If Erin is not white then Erin is nice.
((("Erin" "is" "white" "~")) -> ("Erin" "is" "nice" "+"))
Kind, young people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If someone is red and not blue then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "furry" "+"))
If someone is furry and blue then they are nice.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Red, white people are young.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
Bob is nice.
True
1
proof
[(triple2)]
("Bob" "is" "nice" "+")
triple2
Erin is not kind.
False
1
inv-proof
[(triple13)]
("Erin" "is" "kind" "-")
triple13
Erin is furry.
True
3
proof
[(((triple13 triple15) -> rule4))]
("Erin" "is" "furry" "+")
((triple13 triple15) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
3
inv-proof
[(((triple13 triple15) -> rule4))]
("Erin" "is" "furry" "-")
((triple13 triple15) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Bob is young.
True
4
proof
[(((((triple3) -> rule7) triple3) -> rule8))]
("Bob" "is" "young" "+")
((((triple3) -> (rule7 % int2)) triple3) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule1))]
("Charlie" "is" "furry" "-")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Bob is furry.
True
6
proof
[(((triple1 ((((triple3) -> rule7) triple3) -> rule8)) -> rule4))]
("Bob" "is" "furry" "+")
((triple1 ((((triple3) -> (rule7 % int3)) triple3) -> (rule8 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not furry.
False
6
inv-proof
[(((triple1 ((((triple3) -> rule7) triple3) -> rule8)) -> rule4))]
("Bob" "is" "furry" "-")
((triple1 ((((triple3) -> (rule7 % int3)) triple3) -> (rule8 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "nice" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2)] Bob is white.[(triple3)] Charlie is white.[(triple4)] Charlie is young.[(triple5 OR ((((triple4) -> rule7) triple4) -> rule8))] Dave is blue.[(triple6)] Dave is furry.[(triple7)] Dave is nice.[(triple8 OR ((triple7 triple6) -> rule6))] Dave is red.[(triple9 OR ((triple10) -> rule7))] Dave is white.[(triple10)] Dave is young.[(triple11 OR ((triple9 triple10) -> rule8) OR ((((triple10) -> rule7) triple10) -> rule8))] Erin is blue.[(triple12)] Erin is kind.[(triple13)] Erin is red.[(triple14)] Erin is young.[(triple15)] @1: Bob is red.[(((triple3) -> rule7))] Charlie is red.[(((triple4) -> rule7))] Erin is furry.[(((triple13 triple15) -> rule4))] @2: Bob is young.[(((((triple3) -> rule7) triple3) -> rule8))] Charlie is furry.[(((((triple4) -> rule7)) -> rule1))] Erin is nice.[(((((triple13 triple15) -> rule4) triple12) -> rule6))] @3: Bob is furry.[(((triple1 ((((triple3) -> rule7) triple3) -> rule8)) -> rule4))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((((triple4) -> (rule7 % int2)) triple4) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((triple7 triple6) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple10) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
((triple9 triple10) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple10) -> (rule7 % int2)) triple10) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple12
Erin is kind.
("Erin" "is" "kind" "+")
triple13
Erin is red.
("Erin" "is" "red" "+")
triple14
Erin is young.
("Erin" "is" "young" "+")
triple15
Bob is red.
("Bob" "is" "red" "+")
((triple3) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple4) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple13 triple15) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple3) -> (rule7 % int2)) triple3) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple13 triple15) -> (rule4 % int2)) triple12) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((triple1 ((((triple3) -> (rule7 % int3)) triple3) -> (rule8 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3