Bob is kind. Bob is quiet. Bob is red. Dave is green. Dave is red. Dave is smart. Erin is cold. Erin is kind. Erin is not quiet. Erin is red. Erin is smart. Erin is young. All young things are kind. All red things are young. If Erin is not green then Erin is kind.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Erin is not green then Erin is kind.
((("Erin" "is" "green" "~")) -> ("Erin" "is" "kind" "+"))
Erin is cold.
True
1
proof
[(triple7)]
("Erin" "is" "cold" "+")
triple7
Dave is not red.
False
1
inv-proof
[(triple5)]
("Dave" "is" "red" "-")
triple5
Dave is young.
True
2
proof
[(((triple5) -> rule2))]
("Dave" "is" "young" "+")
((triple5) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "young" "-")
((triple3) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is kind.
True
3
proof
[(((((triple5) -> rule2)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1))]
("Dave" "is" "kind" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is kind.[(triple1 OR ((((triple3) -> rule2)) -> rule1))] Bob is quiet.[(triple2)] Bob is red.[(triple3)] Dave is green.[(triple4)] Dave is red.[(triple5)] Dave is smart.[(triple6)] Erin is cold.[(triple7)] Erin is kind.[(triple8 OR ((triple12) -> rule1) OR ((((triple10) -> rule2)) -> rule1))] Erin is not quiet.[(triple9)] Erin is red.[(triple10)] Erin is smart.[(triple11)] Erin is young.[(triple12 OR ((triple10) -> rule2))] @1: Bob is young.[(((triple3) -> rule2))] Dave is young.[(((triple5) -> rule2))] @2: Dave is kind.[(((((triple5) -> rule2)) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((triple12) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple10) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple3) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple5) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2