Anne is round. Bob is quiet. Erin is not smart. Gary is not smart. All furry, rough things are round. All rough, kind things are round. All rough things are not smart. If something is quiet then it is smart. Round things are not kind. All smart things are not rough. If something is smart and not rough then it is not green. If something is round and not rough then it is not green.
Anne is round.
("Anne" "is" "round" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Gary is not smart.
("Gary" "is" "smart" "-")
All furry, rough things are round.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
All rough, kind things are round.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
All rough things are not smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "-"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Round things are not kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "-"))
All smart things are not rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "-"))
If something is smart and not rough then it is not green.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "green" "-"))
If something is round and not rough then it is not green.
((("something" "is" "round" "+") ("something" "is" "rough" "~")) -> ("something" "is" "green" "-"))
Gary is not smart.
True
1
proof
[(triple4)]
("Gary" "is" "smart" "-")
triple4
Gary is smart.
False
1
inv-proof
[(triple4)]
("Gary" "is" "smart" "+")
triple4
Anne is not kind.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "kind" "-")
((triple1) -> (rule5 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Bob is not smart.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "smart" "-")
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not rough.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("Bob" "is" "rough" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("Bob" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not green.
True
6
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule6)) -> rule7))]
("Bob" "is" "green" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is green.
False
6
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule6)) -> rule7))]
("Bob" "is" "green" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "+")
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "smart" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is round.[(triple1)] Bob is quiet.[(triple2)] Erin is not smart.[(triple3)] Gary is not smart.[(triple4)] @1: Anne is not kind.[(((triple1) -> rule5))] Bob is smart.[(((triple2) -> rule4))] @2: Bob is not rough.[(((((triple2) -> rule4)) -> rule6))] @3: Bob is not green.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule6)) -> rule7))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Erin is not smart.
("Erin" "is" "smart" "-")
triple3
Gary is not smart.
("Gary" "is" "smart" "-")
triple4
Anne is not kind.
("Anne" "is" "kind" "-")
((triple1) -> (rule5 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is not rough.
("Bob" "is" "rough" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is not rough.
("Bob" "is" "rough" "-")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3