Anne is cold. Anne is rough. Bob is kind. Bob is young. Charlie is young. Gary is not cold. Gary is not rough. If something is cold then it is young. If Bob is not kind then Bob is white. All young things are green. Red things are green. Green things are red. If something is red then it is rough.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is not rough.
("Gary" "is" "rough" "-")
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Bob is not kind then Bob is white.
((("Bob" "is" "kind" "~")) -> ("Bob" "is" "white" "+"))
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Gary is not rough.
True
1
proof
[(triple7)]
("Gary" "is" "rough" "-")
triple7
Charlie is not young.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "young" "-")
triple5
Bob is green.
True
2
proof
[(((triple4) -> rule3))]
("Bob" "is" "green" "+")
((triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple4) -> rule3))]
("Bob" "is" "green" "-")
((triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Anne is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule5))]
("Charlie" "is" "red" "-")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Bob is rough.
True
4
proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule6))]
("Bob" "is" "rough" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Anne is not red.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule5))]
("Anne" "is" "red" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule1 <- FAIL)]]
("Gary" "is" "red" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "+")
Gary is not green.
Unknown
inv-rconc
[@4: Gary is green.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule3 <- rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is cold.[(triple1)] Anne is rough.[(triple2 OR ((((((((triple1) -> rule1)) -> rule3)) -> rule5)) -> rule6))] Bob is kind.[(triple3)] Bob is young.[(triple4)] Charlie is young.[(triple5)] Gary is not cold.[(triple6)] Gary is not rough.[(triple7)] @1: Anne is young.[(((triple1) -> rule1))] Bob is green.[(((triple4) -> rule3))] Charlie is green.[(((triple5) -> rule3))] @2: Anne is green.[(((((triple1) -> rule1)) -> rule3))] Bob is red.[(((((triple4) -> rule3)) -> rule5))] Charlie is red.[(((((triple5) -> rule3)) -> rule5))] @3: Anne is red.[(((((((triple1) -> rule1)) -> rule3)) -> rule5))] Bob is rough.[(((((((triple4) -> rule3)) -> rule5)) -> rule6))] Charlie is rough.[(((((((triple5) -> rule3)) -> rule5)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
((((((((triple1) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Gary is not cold.
("Gary" "is" "cold" "-")
triple6
Gary is not rough.
("Gary" "is" "rough" "-")
triple7
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple5) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3