Bob is cold. Dave is rough. Erin is kind. All kind people are round. If someone is round then they are big. All big people are rough.
Bob is cold.
("Bob" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is kind.
("Erin" "is" "kind" "+")
All kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
All big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Erin is not kind.
False
1
inv-proof
[(triple3)]
("Erin" "is" "kind" "-")
triple3
Erin is round.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "round" "+")
((triple3) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "round" "-")
((triple3) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Erin" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Erin" "is" "big" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("Erin" "is" "rough" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not rough.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("Erin" "is" "rough" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "-")
Bob is big.
Unknown
rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "big" "+")
Dave is not big.
Unknown
inv-rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is rough.
Unknown
rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Dave is rough.[(triple2)] Erin is kind.[(triple3)] @1: Erin is round.[(((triple3) -> rule1))] @2: Erin is big.[(((((triple3) -> rule1)) -> rule2))] @3: Erin is rough.[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3