Anne is nice. Bob is rough. Bob is young. Erin is green. Erin is not nice. Gary is rough. Gary is smart. If Gary is round and Gary is furry then Gary is young. If Anne is nice then Anne is furry. If something is young and smart then it is green. If something is young and green then it is rough. Smart, nice things are young. If something is young and not furry then it is not smart. All furry things are smart. If Anne is green and Anne is not young then Anne is not round.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Gary is round and Gary is furry then Gary is young.
((("Gary" "is" "round" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "young" "+"))
If Anne is nice then Anne is furry.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "furry" "+"))
If something is young and smart then it is green.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is young and green then it is rough.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Smart, nice things are young.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is young and not furry then it is not smart.
((("something" "is" "young" "+") ("something" "is" "furry" "~")) -> ("something" "is" "smart" "-"))
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Anne is green and Anne is not young then Anne is not round.
((("Anne" "is" "green" "+") ("Anne" "is" "young" "~")) -> ("Anne" "is" "round" "-"))
Gary is smart.
True
1
proof
[(triple7)]
("Gary" "is" "smart" "+")
triple7
Erin is not green.
False
1
inv-proof
[(triple4)]
("Erin" "is" "green" "-")
triple4
Anne is furry.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule2)) -> rule7))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule7))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
True
5
proof
[(((((((triple1) -> rule2)) -> rule7) triple1) -> rule5))]
("Anne" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not young.
False
5
inv-proof
[(((((((triple1) -> rule2)) -> rule7) triple1) -> rule5))]
("Anne" "is" "young" "-")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
True
9
proof
[(((((((((triple1) -> rule2)) -> rule7) triple1) -> rule5) ((((triple1) -> rule2)) -> rule7)) -> rule3))]
("Anne" "is" "green" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple1) -> (rule5 % int2)) ((((triple1) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is not green.
False
9
inv-proof
[(((((((((triple1) -> rule2)) -> rule7) triple1) -> rule5) ((((triple1) -> rule2)) -> rule7)) -> rule3))]
("Anne" "is" "green" "-")
((((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple1) -> (rule5 % int2)) ((((triple1) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is rough.
True
15
proof
[(((((((((triple1) -> rule2)) -> rule7) triple1) -> rule5) ((((((((triple1) -> rule2)) -> rule7) triple1) -> rule5) ((((triple1) -> rule2)) -> rule7)) -> rule3)) -> rule4))]
("Anne" "is" "rough" "+")
((((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((((triple1) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5
Anne is not rough.
False
15
inv-proof
[(((((((((triple1) -> rule2)) -> rule7) triple1) -> rule5) ((((((((triple1) -> rule2)) -> rule7) triple1) -> rule5) ((((triple1) -> rule2)) -> rule7)) -> rule3)) -> rule4))]
("Anne" "is" "rough" "-")
((((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((((triple1) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "smart" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "young" "-")
Gary is green.
Unknown
rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Gary" "is" "green" "+")
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Bob" "is" "green" "-")
Erin is rough.
Unknown
rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Anne is nice.[(triple1)] Bob is rough.[(triple2)] Bob is young.[(triple3)] Erin is green.[(triple4)] Erin is not nice.[(triple5)] Gary is rough.[(triple6)] Gary is smart.[(triple7)] @1: Anne is furry.[(((triple1) -> rule2))] @2: Anne is smart.[(((((triple1) -> rule2)) -> rule7))] @3: Anne is young.[(((((((triple1) -> rule2)) -> rule7) triple1) -> rule5))] @4: Anne is green.[(((((((((triple1) -> rule2)) -> rule7) triple1) -> rule5) ((((triple1) -> rule2)) -> rule7)) -> rule3))] @5: Anne is rough.[(((((((((triple1) -> rule2)) -> rule7) triple1) -> rule5) ((((((((triple1) -> rule2)) -> rule7) triple1) -> rule5) ((((triple1) -> rule2)) -> rule7)) -> rule3)) -> rule4))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is not nice.
("Erin" "is" "nice" "-")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple1) -> (rule5 % int2)) ((((triple1) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((((triple1) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5