Bob is cold. Bob is red. Dave is red. Dave is young. Erin is smart. Harry is green. Harry is smart. If someone is smart then they are not kind. If someone is smart and not kind then they are not young.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is smart then they are not kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "-"))
If someone is smart and not kind then they are not young.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "young" "-"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple3)]
("Dave" "is" "red" "-")
triple3
Erin is not kind.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "kind" "-")
((triple5) -> (rule1 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is kind.
False
2
inv-proof
[(((triple5) -> rule1))]
("Erin" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is not young.
True
4
proof
[(((triple5 ((triple5) -> rule1)) -> rule2))]
("Erin" "is" "young" "-")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
int2
Erin is young.
False
4
inv-proof
[(((triple5 ((triple5) -> rule1)) -> rule2))]
("Erin" "is" "young" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
int2
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Bob is cold.[(triple1)] Bob is red.[(triple2)] Dave is red.[(triple3)] Dave is young.[(triple4)] Erin is smart.[(triple5)] Harry is green.[(triple6)] Harry is smart.[(triple7)] @1: Erin is not kind.[(((triple5) -> rule1))] Harry is not kind.[(((triple7) -> rule1))] @2: Erin is not young.[(((triple5 ((triple5) -> rule1)) -> rule2))] Harry is not young.[(((triple7 ((triple7) -> rule1)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Erin is smart.
("Erin" "is" "smart" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Erin is not kind.
("Erin" "is" "kind" "-")
((triple5) -> (rule1 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
((triple7) -> (rule1 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Erin is not young.
("Erin" "is" "young" "-")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
int2
Harry is not young.
("Harry" "is" "young" "-")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
int2