Bob is big. Bob is white. Charlie is kind. Charlie is not white. Charlie is young. Dave is big. Erin is not nice. If someone is young and green then they are kind. All white, green people are kind. Kind people are not nice. If someone is blue then they are nice. White people are young. If Dave is big then Dave is white. White, young people are green.
Bob is big.
("Bob" "is" "big" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
If someone is young and green then they are kind.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All white, green people are kind.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Kind people are not nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "-"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
White people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If Dave is big then Dave is white.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "white" "+"))
White, young people are green.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Erin is not nice.
True
1
proof
[(triple7)]
("Erin" "is" "nice" "-")
triple7
Charlie is not kind.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "kind" "-")
triple3
Bob is young.
True
2
proof
[(((triple2) -> rule5))]
("Bob" "is" "young" "+")
((triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is nice.
False
2
inv-proof
[(((triple3) -> rule3))]
("Charlie" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Bob is green.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule7))]
("Bob" "is" "green" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not green.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule7))]
("Bob" "is" "green" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is kind.
True
6
proof
[(((triple2 ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule2) OR ((((triple2) -> rule5) ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule1))]
("Bob" "is" "kind" "+")
((triple2 ((triple2 ((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((triple2) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is not kind.
False
6
inv-proof
[(((triple2 ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule2) OR ((((triple2) -> rule5) ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule1))]
("Bob" "is" "kind" "-")
((triple2 ((triple2 ((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((triple2) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Dave is kind.
True
9
proof
[(((((triple6) -> rule6) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule2) OR ((((((triple6) -> rule6)) -> rule5) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((triple6) -> (rule6 % int4))) -> (rule5 % int3)) ((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Bob is nice.
False
7
inv-proof
[(((((triple2 ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule2)) -> rule3) OR ((((((triple2) -> rule5) ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule1)) -> rule3))]
("Bob" "is" "nice" "+")
((((triple2 ((triple2 ((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
((((((triple2) -> (rule5 % int4)) ((triple2 ((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Dave is not nice.
True
10
proof
[(((((((triple6) -> rule6) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule2)) -> rule3) OR ((((((((triple6) -> rule6)) -> rule5) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule1)) -> rule3))]
("Dave" "is" "nice" "-")
((((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
((((((((triple6) -> (rule6 % int5))) -> (rule5 % int4)) ((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Dave is nice.
False
10
inv-proof
[(((((((triple6) -> rule6) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule2)) -> rule3) OR ((((((((triple6) -> rule6)) -> rule5) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule1)) -> rule3))]
("Dave" "is" "nice" "+")
((((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
((((((((triple6) -> (rule6 % int5))) -> (rule5 % int4)) ((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "young" "+")
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "green" "-")
Erin is kind.
Unknown
rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Erin" "is" "kind" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Bob is big.[(triple1)] Bob is white.[(triple2)] Charlie is kind.[(triple3)] Charlie is not white.[(triple4)] Charlie is young.[(triple5)] Dave is big.[(triple6)] Erin is not nice.[(triple7)] @1: Bob is young.[(((triple2) -> rule5))] Charlie is not nice.[(((triple3) -> rule3))] Dave is white.[(((triple6) -> rule6))] @2: Bob is green.[(((triple2 ((triple2) -> rule5)) -> rule7))] Dave is young.[(((((triple6) -> rule6)) -> rule5))] @3: Bob is kind.[(((triple2 ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule2) OR ((((triple2) -> rule5) ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule1))] Dave is green.[(((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7))] @4: Bob is not nice.[(((((triple2 ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule2)) -> rule3) OR ((((((triple2) -> rule5) ((triple2 ((triple2) -> rule5)) -> rule7)) -> rule1)) -> rule3))] Dave is kind.[(((((triple6) -> rule6) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule2) OR ((((((triple6) -> rule6)) -> rule5) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule1))] @5: Dave is not nice.[(((((((triple6) -> rule6) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule2)) -> rule3) OR ((((((((triple6) -> rule6)) -> rule5) ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule7)) -> rule1)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is not white.
("Charlie" "is" "white" "-")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Erin is not nice.
("Erin" "is" "nice" "-")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
((triple3) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple6) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple2 ((triple2 ((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((triple2) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((triple6) -> (rule6 % int3)) ((((triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Bob is not nice.
("Bob" "is" "nice" "-")
((((triple2 ((triple2 ((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
((((((triple2) -> (rule5 % int4)) ((triple2 ((triple2) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((triple6) -> (rule6 % int4))) -> (rule5 % int3)) ((((triple6) -> (rule6 % int4)) ((((triple6) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is not nice.
("Dave" "is" "nice" "-")
((((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
((((((((triple6) -> (rule6 % int5))) -> (rule5 % int4)) ((((triple6) -> (rule6 % int5)) ((((triple6) -> (rule6 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5