Anne is green. Bob is not blue. Bob is young. Charlie is nice. Charlie is rough. Dave is cold. Dave is not rough. All cold people are young. If Dave is young and Dave is cold then Dave is blue. Young, cold people are round. If someone is blue and cold then they are green. If someone is cold and rough then they are not green. If Anne is blue and Anne is not round then Anne is not rough.
Anne is green.
("Anne" "is" "green" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is young.
("Bob" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If Dave is young and Dave is cold then Dave is blue.
((("Dave" "is" "young" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "blue" "+"))
Young, cold people are round.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is blue and cold then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is cold and rough then they are not green.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
If Anne is blue and Anne is not round then Anne is not rough.
((("Anne" "is" "blue" "+") ("Anne" "is" "round" "~")) -> ("Anne" "is" "rough" "-"))
Dave is not rough.
True
1
proof
[(triple7)]
("Dave" "is" "rough" "-")
triple7
Dave is rough.
False
1
inv-proof
[(triple7)]
("Dave" "is" "rough" "+")
triple7
Dave is young.
True
2
proof
[(((triple6) -> rule1))]
("Dave" "is" "young" "+")
((triple6) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple6) -> rule1))]
("Dave" "is" "young" "-")
((triple6) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
True
4
proof
[(((((triple6) -> rule1) triple6) -> rule2))]
("Dave" "is" "blue" "+")
((((triple6) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((((triple6) -> rule1) triple6) -> rule2))]
("Dave" "is" "blue" "-")
((((triple6) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
True
6
proof
[(((((((triple6) -> rule1) triple6) -> rule2) triple6) -> rule4))]
("Dave" "is" "green" "+")
((((((triple6) -> (rule1 % int3)) triple6) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not green.
False
6
inv-proof
[(((((((triple6) -> rule1) triple6) -> rule2) triple6) -> rule4))]
("Dave" "is" "green" "-")
((((((triple6) -> (rule1 % int3)) triple6) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "round" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "young" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "round" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Anne is green.[(triple1)] Bob is not blue.[(triple2)] Bob is young.[(triple3)] Charlie is nice.[(triple4)] Charlie is rough.[(triple5)] Dave is cold.[(triple6)] Dave is not rough.[(triple7)] @1: Dave is young.[(((triple6) -> rule1))] @2: Dave is blue.[(((((triple6) -> rule1) triple6) -> rule2))] Dave is round.[(((((triple6) -> rule1) triple6) -> rule3))] @3: Dave is green.[(((((((triple6) -> rule1) triple6) -> rule2) triple6) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is not blue.
("Bob" "is" "blue" "-")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is not rough.
("Dave" "is" "rough" "-")
triple7
Dave is young.
("Dave" "is" "young" "+")
((triple6) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple6) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple6) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((((triple6) -> (rule1 % int3)) triple6) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3