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