Bob is round. Charlie is green. Charlie is not round. Charlie is not smart. Dave is nice. Dave is round. Dave is not white. Erin is round. Erin is smart. Erin is not white. If someone is smart then they are not young.
Bob is round.
("Bob" "is" "round" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not white.
("Dave" "is" "white" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is not white.
("Erin" "is" "white" "-")
If someone is smart then they are not young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "-"))
Dave is nice.
True
1
proof
[(triple5)]
("Dave" "is" "nice" "+")
triple5
Erin is white.
False
1
inv-proof
[(triple10)]
("Erin" "is" "white" "+")
triple10
Erin is not young.
True
2
proof
[(((triple9) -> rule1))]
("Erin" "is" "young" "-")
((triple9) -> (rule1 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is young.
False
2
inv-proof
[(((triple9) -> rule1))]
("Erin" "is" "young" "+")
((triple9) -> (rule1 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is round.[(triple1)] Charlie is green.[(triple2)] Charlie is not round.[(triple3)] Charlie is not smart.[(triple4)] Dave is nice.[(triple5)] Dave is not white.[(triple7)] Dave is round.[(triple6)] Erin is not white.[(triple10)] Erin is round.[(triple8)] Erin is smart.[(triple9)] @1: Erin is not young.[(((triple9) -> rule1))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is not round.
("Charlie" "is" "round" "-")
triple3
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not white.
("Dave" "is" "white" "-")
triple7
Dave is round.
("Dave" "is" "round" "+")
triple6
Erin is not white.
("Erin" "is" "white" "-")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple8
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Erin is not young.
("Erin" "is" "young" "-")
((triple9) -> (rule1 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1