Anne is kind. Anne is white. Anne is young. Bob is quiet. Bob is smart. Bob is young. Erin is blue. Erin is nice. Erin is quiet. Erin is smart. Erin is white. Erin is young. All young things are nice. If something is nice then it is kind. If Erin is nice and Erin is quiet then Erin is white. All nice, blue things are white. Young things are white. All young things are nice.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If Erin is nice and Erin is quiet then Erin is white.
((("Erin" "is" "nice" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "white" "+"))
All nice, blue things are white.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Bob is smart.
True
1
proof
[(triple5)]
("Bob" "is" "smart" "+")
triple5
Bob is not quiet.
False
1
inv-proof
[(triple4)]
("Bob" "is" "quiet" "-")
triple4
Erin is kind.
True
2
proof
[(((triple8) -> rule2) OR ((((triple12) -> rule1)) -> rule2) OR ((((triple12) -> rule6)) -> rule2))]
("Erin" "is" "kind" "+")
((triple8) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Bob is not white.
False
2
inv-proof
[(((triple6) -> rule5))]
("Bob" "is" "white" "-")
((triple6) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
True
3
proof
[(((((triple6) -> rule1)) -> rule2) OR ((((triple6) -> rule6)) -> rule2))]
("Bob" "is" "kind" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule2) OR ((((triple6) -> rule6)) -> rule2))]
("Bob" "is" "kind" "-")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is kind.[(triple1 OR ((((triple3) -> rule1)) -> rule2) OR ((((triple3) -> rule6)) -> rule2))] Anne is white.[(triple2 OR ((triple3) -> rule5))] Anne is young.[(triple3)] Bob is quiet.[(triple4)] Bob is smart.[(triple5)] Bob is young.[(triple6)] Erin is blue.[(triple7)] Erin is nice.[(triple8 OR ((triple12) -> rule1) OR ((triple12) -> rule6))] Erin is quiet.[(triple9)] Erin is smart.[(triple10)] Erin is white.[(triple11 OR ((triple12) -> rule5) OR ((triple8 triple7) -> rule4) OR ((triple8 triple9) -> rule3) OR ((((triple12) -> rule1) triple7) -> rule4) OR ((((triple12) -> rule1) triple9) -> rule3) OR ((((triple12) -> rule6) triple7) -> rule4) OR ((((triple12) -> rule6) triple9) -> rule3))] Erin is young.[(triple12)] @1: Anne is nice.[(((triple3) -> rule1) OR ((triple3) -> rule6))] Bob is nice.[(((triple6) -> rule1) OR ((triple6) -> rule6))] Bob is white.[(((triple6) -> rule5))] Erin is kind.[(((triple8) -> rule2) OR ((((triple12) -> rule1)) -> rule2) OR ((((triple12) -> rule6)) -> rule2))] @2: Bob is kind.[(((((triple6) -> rule1)) -> rule2) OR ((((triple6) -> rule6)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple2
((triple3) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((triple12) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple12) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is white.
("Erin" "is" "white" "+")
triple11
((triple12) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple8 triple7) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple8 triple9) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple12) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple12) -> (rule1 % int2)) triple9) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple12) -> (rule6 % int2)) triple7) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple12) -> (rule6 % int2)) triple9) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple12
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple3) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple6) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple6) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple8) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2