Bob is rough. Charlie is not cold. Erin is round. Round things are kind. Cold things are kind. If something is rough then it is cold. If something is kind then it is rough. Green, round things are rough. Round things are not young. If something is nice and not kind then it is young. If something is cold and not kind then it is nice.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Erin is round.
("Erin" "is" "round" "+")
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Green, round things are rough.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Round things are not young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "-"))
If something is nice and not kind then it is young.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "young" "+"))
If something is cold and not kind then it is nice.
((("something" "is" "cold" "+") ("something" "is" "kind" "~")) -> ("something" "is" "nice" "+"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Charlie is cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Erin is kind.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is rough.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("Erin" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Erin is cold.
True
4
proof
[(((((((triple3) -> rule1)) -> rule4)) -> rule3))]
("Erin" "is" "cold" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not cold.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule4)) -> rule3))]
("Erin" "is" "cold" "-")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "young" "-")
Charlie is rough.
Unknown
rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
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" "+")
@0: Bob is rough.[(triple1)] Charlie is not cold.[(triple2)] Erin is round.[(triple3)] @1: Bob is cold.[(((triple1) -> rule3))] Erin is kind.[(((triple3) -> rule1))] Erin is not young.[(((triple3) -> rule6))] @2: Bob is kind.[(((((triple1) -> rule3)) -> rule2))] Erin is rough.[(((((triple3) -> rule1)) -> rule4))] @3: Erin is cold.[(((((((triple3) -> rule1)) -> rule4)) -> rule3))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
((triple3) -> (rule6 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3