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