Bob is cold. Bob is green. Bob is kind. Bob is white. Bob is young. Erin is green. Erin is kind. Erin is nice. Erin is white. Erin is young. Young, white people are nice. All nice, white people are young. If Erin is white then Erin is young. If Bob is cold and Bob is green then Bob is kind. Kind people are green. All nice, quiet people are white. Kind, white people are nice. Green people are cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Young, white people are nice.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
All nice, white people are young.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If Erin is white then Erin is young.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "young" "+"))
If Bob is cold and Bob is green then Bob is kind.
((("Bob" "is" "cold" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "kind" "+"))
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All nice, quiet people are white.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Kind, white people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Erin is green.
True
1
proof
[(triple6 OR ((triple7) -> rule5))]
("Erin" "is" "green" "+")
triple6
((triple7) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Bob is not kind.
False
1
inv-proof
[(triple3 OR ((triple1 triple2) -> rule4) OR ((((triple2) -> rule8) triple2) -> rule4))]
("Bob" "is" "kind" "-")
triple3
((triple1 triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule8 % int2)) triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Erin is cold.
True
2
proof
[(((triple6) -> rule8) OR ((((triple7) -> rule5)) -> rule8))]
("Erin" "is" "cold" "+")
((triple6) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((triple3 triple4) -> rule7) OR ((triple5 triple4) -> rule1) OR ((((triple1 triple2) -> rule4) triple4) -> rule7) OR ((((((triple2) -> rule8) triple2) -> rule4) triple4) -> rule7))]
("Bob" "is" "nice" "-")
((triple3 triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple5 triple4) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1 triple2) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple2) -> (rule8 % int3)) triple2) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Bob is cold.[(triple1 OR ((triple2) -> rule8) OR ((((triple3) -> rule5)) -> rule8))] Bob is green.[(triple2 OR ((triple3) -> rule5))] Bob is kind.[(triple3 OR ((triple1 triple2) -> rule4) OR ((((triple2) -> rule8) triple2) -> rule4))] Bob is white.[(triple4)] Bob is young.[(triple5 OR ((((triple3 triple4) -> rule7) triple4) -> rule2) OR ((((((triple1 triple2) -> rule4) triple4) -> rule7) triple4) -> rule2) OR ((((((((triple2) -> rule8) triple2) -> rule4) triple4) -> rule7) triple4) -> rule2))] Erin is green.[(triple6 OR ((triple7) -> rule5))] Erin is kind.[(triple7)] Erin is nice.[(triple8 OR ((triple10 triple9) -> rule1) OR ((triple7 triple9) -> rule7) OR ((((triple9) -> rule3) triple9) -> rule1))] Erin is white.[(triple9)] Erin is young.[(triple10 OR ((triple9) -> rule3) OR ((triple8 triple9) -> rule2) OR ((((triple7 triple9) -> rule7) triple9) -> rule2))] @1: Bob is nice.[(((triple3 triple4) -> rule7) OR ((triple5 triple4) -> rule1) OR ((((triple1 triple2) -> rule4) triple4) -> rule7) OR ((((((triple2) -> rule8) triple2) -> rule4) triple4) -> rule7))] Erin is cold.[(((triple6) -> rule8) OR ((((triple7) -> rule5)) -> rule8))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple3) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple1 triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule8 % int2)) triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
((((triple3 triple4) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple1 triple2) -> (rule4 % int3)) triple4) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((((triple2) -> (rule8 % int4)) triple2) -> (rule4 % int3)) triple4) -> (rule7 % int2)) triple4) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
triple6
((triple7) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((triple10 triple9) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple7 triple9) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple9) -> (rule3 % int2)) triple9) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple9) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple8 triple9) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple7 triple9) -> (rule7 % int2)) triple9) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((triple3 triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple5 triple4) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1 triple2) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple2) -> (rule8 % int3)) triple2) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((triple6) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2