Bob is nice. Charlie is rough. Dave is not cold. Erin is furry. All big things are rough. All furry things are nice. All nice things are cold. If something is smart and not big then it is furry. Rough things are furry. Big, nice things are furry. If Erin is big then Erin is smart. If Charlie is furry then Charlie is nice.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Erin is furry.
("Erin" "is" "furry" "+")
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is smart and not big then it is furry.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "furry" "+"))
Rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Big, nice things are furry.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Erin is big then Erin is smart.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "smart" "+"))
If Charlie is furry then Charlie is nice.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "nice" "+"))
Erin is furry.
True
1
proof
[(triple4)]
("Erin" "is" "furry" "+")
triple4
Charlie is not rough.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "rough" "-")
triple2
Charlie is furry.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "furry" "-")
((triple2) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is cold.
True
3
proof
[(((((triple4) -> rule2)) -> rule3))]
("Erin" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not cold.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule3))]
("Erin" "is" "cold" "-")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Charlie is cold.
True
4
proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule3) OR ((((((triple2) -> rule5)) -> rule8)) -> rule3))]
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not cold.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule3) OR ((((((triple2) -> rule5)) -> rule8)) -> rule3))]
("Charlie" "is" "cold" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "+")
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "smart" "-")
Dave is nice.
Unknown
rconc
[@3: Dave is nice.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- FAIL)]]
("Dave" "is" "nice" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Bob is nice.[(triple1)] Charlie is rough.[(triple2)] Dave is not cold.[(triple3)] Erin is furry.[(triple4)] @1: Bob is cold.[(((triple1) -> rule3))] Charlie is furry.[(((triple2) -> rule5))] Erin is nice.[(((triple4) -> rule2))] @2: Charlie is nice.[(((((triple2) -> rule5)) -> rule2) OR ((((triple2) -> rule5)) -> rule8))] Erin is cold.[(((((triple4) -> rule2)) -> rule3))] @3: Charlie is cold.[(((((((triple2) -> rule5)) -> rule2)) -> rule3) OR ((((((triple2) -> rule5)) -> rule8)) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is not cold.
("Dave" "is" "cold" "-")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple4) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3