Bob is quiet. Charlie is cold. Dave is furry. Harry is nice. If something is young then it is cold. Cold things are not quiet. Blue things are quiet. If something is quiet then it is nice. If something is quiet and not young then it is nice. If something is smart and young then it is blue. All furry things are blue. If Dave is young and Dave is nice then Dave is not quiet.
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Cold things are not quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "-"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is quiet and not young then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "young" "~")) -> ("something" "is" "nice" "+"))
If something is smart and young then it is blue.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
If Dave is young and Dave is nice then Dave is not quiet.
((("Dave" "is" "young" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "quiet" "-"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Charlie is not quiet.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Bob is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple3) -> rule7)) -> rule3))]
("Dave" "is" "quiet" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3))]
("Dave" "is" "quiet" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
True
4
proof
[(((((((triple3) -> rule7)) -> rule3)) -> rule4))]
("Dave" "is" "nice" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not nice.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule3)) -> rule4))]
("Dave" "is" "nice" "-")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "blue" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is quiet.[(triple1)] Charlie is cold.[(triple2)] Dave is furry.[(triple3)] Harry is nice.[(triple4)] @1: Bob is nice.[(((triple1) -> rule4))] Charlie is not quiet.[(((triple2) -> rule2))] Dave is blue.[(((triple3) -> rule7))] @2: Dave is quiet.[(((((triple3) -> rule7)) -> rule3))] @3: Dave is nice.[(((((((triple3) -> rule7)) -> rule3)) -> rule4))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple3) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3