Bob is cold. Bob is green. Bob is not kind. Bob is not nice. Bob is not young. Dave is kind. Dave is not rough. Erin is not cold. Erin is kind. Erin is nice. Erin is not rough. Erin is young. Nice, green people are not cold. Green, quiet people are rough. If Bob is nice and Bob is cold then Bob is young. If someone is kind then they are nice. If someone is quiet and not rough then they are not young. Nice people are young.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is not kind.
("Bob" "is" "kind" "-")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is not young.
("Bob" "is" "young" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is young.
("Erin" "is" "young" "+")
Nice, green people are not cold.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "-"))
Green, quiet people are rough.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If Bob is nice and Bob is cold then Bob is young.
((("Bob" "is" "nice" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "young" "+"))
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet and not rough then they are not young.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "young" "-"))
Nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Bob is not nice.
True
1
proof
[(triple4)]
("Bob" "is" "nice" "-")
triple4
Erin is rough.
False
1
inv-proof
[(triple11)]
("Erin" "is" "rough" "+")
triple11
Dave is nice.
True
2
proof
[(((triple6) -> rule4))]
("Dave" "is" "nice" "+")
((triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple6) -> rule4))]
("Dave" "is" "nice" "-")
((triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
True
3
proof
[(((((triple6) -> rule4)) -> rule6))]
("Dave" "is" "young" "+")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not young.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule6))]
("Dave" "is" "young" "-")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is not kind.[(triple3)] Bob is not nice.[(triple4)] Bob is not young.[(triple5)] Dave is kind.[(triple6)] Dave is not rough.[(triple7)] Erin is kind.[(triple9)] Erin is nice.[(triple10 OR ((triple9) -> rule4))] Erin is not cold.[(triple8)] Erin is not rough.[(triple11)] Erin is young.[(triple12 OR ((triple10) -> rule6) OR ((((triple9) -> rule4)) -> rule6))] @1: Dave is nice.[(((triple6) -> rule4))] @2: Dave is young.[(((((triple6) -> rule4)) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is not kind.
("Bob" "is" "kind" "-")
triple3
Bob is not nice.
("Bob" "is" "nice" "-")
triple4
Bob is not young.
("Bob" "is" "young" "-")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is not rough.
("Dave" "is" "rough" "-")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
((triple9) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
triple8
Erin is not rough.
("Erin" "is" "rough" "-")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple10) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2