Bob is kind. Charlie is smart. If something is quiet then it is round. If something is furry then it is cold. If something is round then it is furry. All furry, smart things are rough. All furry, kind things are quiet. If something is furry and rough then it is round. Kind things are quiet. If something is smart then it is furry.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If something is quiet then it is round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All furry, smart things are rough.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
All furry, kind things are quiet.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is furry and rough then it is round.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Charlie is smart.
True
1
proof
[(triple2)]
("Charlie" "is" "smart" "+")
triple2
Charlie is not smart.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "smart" "-")
triple2
Charlie is furry.
True
2
proof
[(((triple2) -> rule8))]
("Charlie" "is" "furry" "+")
((triple2) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple2) -> rule8))]
("Charlie" "is" "furry" "-")
((triple2) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Bob is round.
True
3
proof
[(((((triple1) -> rule7)) -> rule1))]
("Bob" "is" "round" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule1))]
("Bob" "is" "round" "-")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Charlie is round.
True
7
proof
[(((((triple2) -> rule8) ((((triple2) -> rule8) triple2) -> rule4)) -> rule6))]
("Charlie" "is" "round" "+")
((((triple2) -> (rule8 % int3)) ((((triple2) -> (rule8 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not round.
False
7
inv-proof
[(((((triple2) -> rule8) ((((triple2) -> rule8) triple2) -> rule4)) -> rule6))]
("Charlie" "is" "round" "-")
((((triple2) -> (rule8 % int3)) ((((triple2) -> (rule8 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "rough" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is kind.[(triple1)] Charlie is smart.[(triple2)] @1: Bob is quiet.[(((triple1) -> rule7))] Charlie is furry.[(((triple2) -> rule8))] @2: Bob is round.[(((((triple1) -> rule7)) -> rule1))] Charlie is cold.[(((((triple2) -> rule8)) -> rule2))] Charlie is rough.[(((((triple2) -> rule8) triple2) -> rule4))] @3: Bob is furry.[(((((((triple1) -> rule7)) -> rule1)) -> rule3))] Charlie is round.[(((((triple2) -> rule8) ((((triple2) -> rule8) triple2) -> rule4)) -> rule6))] @4: Bob is cold.[(((((((((triple1) -> rule7)) -> rule1)) -> rule3)) -> rule2))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple2) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule8 % int2)) triple2) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((((triple2) -> (rule8 % int3)) ((((triple2) -> (rule8 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4