Bob is smart. Dave is kind. Erin is young. Gary is young. Round, cold people are young. All kind, nice people are smart. Round people are cold. All smart people are round. Nice people are young. Cold, young people are rough. Kind, nice people are rough. Young, smart people are cold.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is young.
("Gary" "is" "young" "+")
Round, cold people are young.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All kind, nice people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Cold, young people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Kind, nice people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Young, smart people are cold.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Gary is young.
True
1
proof
[(triple4)]
("Gary" "is" "young" "+")
triple4
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Bob is round.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "round" "-")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Bob" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("Bob" "is" "cold" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
True
6
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule1))]
("Bob" "is" "young" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not young.
False
6
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule1))]
("Bob" "is" "young" "-")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@3: Erin is cold.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule2 <- FAIL)]]
("Erin" "is" "cold" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not rough.
Unknown
inv-rconc
[@4: Dave is rough.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule4 <- rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Gary is rough.
Unknown
rconc
[@4: Gary is rough.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule4 <- rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Bob is smart.[(triple1)] Dave is kind.[(triple2)] Erin is young.[(triple3)] Gary is young.[(triple4)] @1: Bob is round.[(((triple1) -> rule4))] @2: Bob is cold.[(((((triple1) -> rule4)) -> rule3))] @3: Bob is young.[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule1))] @4: Bob is rough.[(((((((triple1) -> rule4)) -> rule3) ((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple1) -> (rule4 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4