Bob is furry. Bob is white. Dave is not kind. Dave is nice. Erin is nice. Erin is white. Harry is blue. Harry is cold. Harry is furry. Harry is white. If something is kind then it is not blue. All furry things are white. If Bob is white then Bob is kind. If Harry is white and Harry is quiet then Harry is not cold. If Bob is not blue then Bob is quiet. All cold things are nice. All quiet things are cold.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is kind then it is not blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "-"))
All furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If Bob is white then Bob is kind.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "kind" "+"))
If Harry is white and Harry is quiet then Harry is not cold.
((("Harry" "is" "white" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "cold" "-"))
If Bob is not blue then Bob is quiet.
((("Bob" "is" "blue" "~")) -> ("Bob" "is" "quiet" "+"))
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Bob is white.
True
1
proof
[(triple2 OR ((triple1) -> rule2))]
("Bob" "is" "white" "+")
triple2
((triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Bob is kind.
True
2
proof
[(((triple2) -> rule3) OR ((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule3) OR ((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not blue.
True
3
proof
[(((((triple2) -> rule3)) -> rule1) OR ((((((triple1) -> rule2)) -> rule3)) -> rule1))]
("Bob" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is blue.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1) OR ((((((triple1) -> rule2)) -> rule3)) -> rule1))]
("Bob" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is quiet.
True
4
proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule5) OR ((((((((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5))]
("Bob" "is" "quiet" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is not quiet.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule5) OR ((((((((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5))]
("Bob" "is" "quiet" "-")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is cold.
True
5
proof
[(((((((((triple2) -> rule3)) -> rule1)) -> rule5)) -> rule7) OR ((((((((((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5)) -> rule7))]
("Bob" "is" "cold" "+")
((((((((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not blue.
("Bob" "is" "blue" "-")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
((((((((((triple1) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not blue.
("Bob" "is" "blue" "-")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is not cold.
False
5
inv-proof
[(((((((((triple2) -> rule3)) -> rule1)) -> rule5)) -> rule7) OR ((((((((((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5)) -> rule7))]
("Bob" "is" "cold" "-")
((((((((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not blue.
("Bob" "is" "blue" "-")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
((((((((((triple1) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not blue.
("Bob" "is" "blue" "-")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is nice.
True
6
proof
[(((((((((((triple2) -> rule3)) -> rule1)) -> rule5)) -> rule7)) -> rule6) OR ((((((((((((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5)) -> rule7)) -> rule6))]
("Bob" "is" "nice" "+")
((((((((((triple2) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not blue.
("Bob" "is" "blue" "-")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
((((((((((((triple1) -> (rule2 % int6))) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not blue.
("Bob" "is" "blue" "-")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is white.
("Bob" "is" "white" "+")
int6
Bob is not nice.
False
6
inv-proof
[(((((((((((triple2) -> rule3)) -> rule1)) -> rule5)) -> rule7)) -> rule6) OR ((((((((((((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5)) -> rule7)) -> rule6))]
("Bob" "is" "nice" "-")
((((((((((triple2) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not blue.
("Bob" "is" "blue" "-")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
((((((((((((triple1) -> (rule2 % int6))) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not blue.
("Bob" "is" "blue" "-")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is white.
("Bob" "is" "white" "+")
int6
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "cold" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "+")
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "cold" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Bob is furry.[(triple1)] Bob is white.[(triple2 OR ((triple1) -> rule2))] Dave is nice.[(triple4)] Dave is not kind.[(triple3)] Erin is nice.[(triple5)] Erin is white.[(triple6)] Harry is blue.[(triple7)] Harry is cold.[(triple8)] Harry is furry.[(triple9)] Harry is white.[(triple10 OR ((triple9) -> rule2))] @1: Bob is kind.[(((triple2) -> rule3) OR ((((triple1) -> rule2)) -> rule3))] Harry is nice.[(((triple8) -> rule6))] @2: Bob is not blue.[(((((triple2) -> rule3)) -> rule1) OR ((((((triple1) -> rule2)) -> rule3)) -> rule1))] @3: Bob is quiet.[(((((((triple2) -> rule3)) -> rule1)) -> rule5) OR ((((((((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5))] @4: Bob is cold.[(((((((((triple2) -> rule3)) -> rule1)) -> rule5)) -> rule7) OR ((((((((((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5)) -> rule7))] @5: Bob is nice.[(((((((((((triple2) -> rule3)) -> rule1)) -> rule5)) -> rule7)) -> rule6) OR ((((((((((((triple1) -> rule2)) -> rule3)) -> rule1)) -> rule5)) -> rule7)) -> rule6))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
((triple1) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is not kind.
("Dave" "is" "kind" "-")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple9) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple8) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
((((((((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not blue.
("Bob" "is" "blue" "-")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
((((((((((triple1) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not blue.
("Bob" "is" "blue" "-")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
Bob is nice.
("Bob" "is" "nice" "+")
((((((((((triple2) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not blue.
("Bob" "is" "blue" "-")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
((((((((((((triple1) -> (rule2 % int6))) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not blue.
("Bob" "is" "blue" "-")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is white.
("Bob" "is" "white" "+")
int6