Dave is smart. Erin is furry. If Erin is white then Erin is rough. If something is round then it is white. All furry things are round.
Dave is smart.
("Dave" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
If Erin is white then Erin is rough.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "rough" "+"))
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Erin is furry.
True
1
proof
[(triple2)]
("Erin" "is" "furry" "+")
triple2
Dave is not smart.
False
1
inv-proof
[(triple1)]
("Dave" "is" "smart" "-")
triple1
Erin is round.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "round" "+")
((triple2) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "round" "-")
((triple2) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Erin" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Erin" "is" "white" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
True
4
proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule1))]
("Erin" "is" "rough" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not rough.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule1))]
("Erin" "is" "rough" "-")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "white" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Dave is smart.[(triple1)] Erin is furry.[(triple2)] @1: Erin is round.[(((triple2) -> rule3))] @2: Erin is white.[(((((triple2) -> rule3)) -> rule2))] @3: Erin is rough.[(((((((triple2) -> rule3)) -> rule2)) -> rule1))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3